POLA violation on conjunctive theorems

[chaudhuri]

The following seems to violate the principle of least astonishment.

Kind i type.
Type c i.
Type f i -> i.
Type p i -> prop.
Type q i -> i -> prop.

Theorem t1 : true /\ true. search.
Theorem t2 : true /\ (forall x, p x). skip.
Theorem t3 : (forall x, p x) /\ (forall x y, q x y). skip.
Theorem t4 : (forall x y, q x y) -> c = f c. skip.

Theorem test : false.
apply 0 t1.   % goal is unchanged!

apply 0 t2.   % H1 : forall x, p x

apply 0 t3.   % H2 : forall x, p x
              % H3 : forall x y, q x y

apply 0 t4 to H3. % proof completed!

In all these cases we would have expected the structure of the applied theorems to be preserved in the hypotheses, not eagerly simplified using left-asynchronous rules.