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.
The following seems to violate the principle of least astonishment.
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.