contribution about \lambda-\delta

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pr3_subst1.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v
new file mode 100644 (file)
index 0000000..78c9834
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v
@@ -0,0 +1,33 @@
+(*#* #stop file *)
+
+Require subst1_defs.
+Require pr2_subst1.
+Require pr3_defs.
+
+   Section pr3_subst1_props. (***********************************************)
+
+      Theorem pr3_subst1: (c,e:?; v:?; i:?) (drop i (0) c (CTail e (Bind Abbr) v)) ->
+                          (t1,t2:?) (pr3 c t1 t2) ->
+                          (w1:?) (subst1 i v t1 w1) ->
+                          (EX w2 | (pr3 c w1 w2) & (subst1 i v t2 w2)).
+     Intros until 2; XElim H0; Clear t1 t2; Intros.
+(* case 1: pr3_refl *)
+     XEAuto.
+(* case 2: pr3_single *)
+     Pr2Subst1.
+     LApply (H2 x); [ Clear H2; Intros H2 | XAuto ].
+     XElim H2; XEAuto.
+     Qed.
+
+   End pr3_subst1_props.
+
+      Tactic Definition Pr3Subst1 :=
+         Match Context With
+            | [ H0: (drop ?1 (0) ?2 (CTail ?3 (Bind Abbr) ?4));
+                H1: (pr3 ?2 ?5 ?6); H3: (subst1 ?1 ?4 ?5 ?7) |- ? ] ->
+               LApply (pr3_subst1 ?2 ?3 ?4 ?1); [ Intros H_x | XAuto ];
+               LApply (H_x ?5 ?6); [ Clear H_x H1; Intros H1 | XAuto ];
+               LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ];
+               XElim H1; Intros
+            | _ -> Pr2Subst1.
+