Mercurial > cpdt > repo

comparison src/Firstorder.v @ 183:02569049397b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Closure conversion defined
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 14:01:33 -0500
parents 6087a32b1926
children 13620dfd5f97
comparison
equal deleted inserted replaced
182:24b99e025fe8 183:02569049397b
144 -> G1 ++ (x, xt) :: nil |-v x' : t 144 -> G1 ++ (x, xt) :: nil |-v x' : t
145 -> t = xt. 145 -> t = xt.
146 induction G1 as [ | [x'' t'] tl ]; crush; eauto; 146 induction G1 as [ | [x'' t'] tl ]; crush; eauto;
147 match goal with 147 match goal with
148 | [ H : _ |-v _ : _ |- _ ] => inversion H 148 | [ H : _ |-v _ : _ |- _ ] => inversion H
149 end; crush; elimtype False; eauto; 149 end; crush; (elimtype False; eauto;
150 match goal with 150 match goal with
151 | [ H : nil |-v _ : _ |- _ ] => inversion H 151 | [ H : nil |-v _ : _ |- _ ] => inversion H
152 end. 152 end)
153 || match goal with
154 | [ H : _ |- _ ] => apply H; crush; eauto
155 end.
153 Qed. 156 Qed.
154 157
155 Implicit Arguments subst_lookup [x' t G1]. 158 Implicit Arguments subst_lookup [x' t G1].
156 159
157 Lemma shadow_lookup : forall v t t' G1, 160 Lemma shadow_lookup : forall v t t' G1,