Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 548:a43fd2ba7ad3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Working again with Coq 8.4
author Adam Chlipala <adam@chlipala.net>
date Wed, 12 Jul 2017 13:33:23 -0400
parents 2c8c693ddaba
children 16d701d4bd82
comparison
equal deleted inserted replaced
547:2c8c693ddaba 548:a43fd2ba7ad3
820 -> exec (Bnd m (fun x => Bnd (f x) g)) r. 820 -> exec (Bnd m (fun x => Bnd (f x) g)) r.
821 induction 1; crush. 821 induction 1; crush.
822 match goal with 822 match goal with
823 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst 823 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
824 end. 824 end.
825 subst B.
825 crush. 826 crush.
826 inversion H; clear H; crush. 827 inversion H; clear H; crush.
827 eauto. 828 eauto.
828 Qed. 829 Qed.
829 830
833 -> exec (Bnd (Bnd m f) g) r. 834 -> exec (Bnd (Bnd m f) g) r.
834 induction 1; crush. 835 induction 1; crush.
835 match goal with 836 match goal with
836 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst 837 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
837 end. 838 end.
839 subst A.
838 crush. 840 crush.
839 inversion H0; clear H0; crush. 841 inversion H0; clear H0; crush.
840 eauto. 842 eauto.
841 Qed. 843 Qed.
842 844