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
Last updated: Feb 08 2023 at 07:02 UTC