Suppose I have something like
Parameter X Y Z: Set.
Axiom foo : X -> Y -> Z.
Axiom x : X.
Axiom y : Y.
Lemma test : Z.
Proof.
apply/foo/y/x.
Qed.
Why do chained apply
views work on the last generated goal rather than the top one, i.e. the proof above works but apply/foo/x/y
doesn't?
Last updated: Mar 28 2024 at 12:01 UTC