contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
new file mode 100644 (file)
index 0000000..4e26ce7
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
@@ -0,0 +1,22 @@
+(*#* #stop file *)
+
+Require subst1_confluence.
+Require csubst1_defs.
+Require pr3_gen_context.
+Require pc3_defs.
+Require pc3_props.
+
+   Section pc3_gen_context. (************************************************)
+
+      Theorem pc3_gen_cabbr: (c:?; t1,t2:?) (pc3 c t1 t2) -> (e:?; u:?; d:?)
+                             (drop d (0) c (CTail e (Bind Abbr) u)) ->
+                             (a0:?) (csubst1 d u c a0) ->
+                             (a:?) (drop (1) d a0 a) ->
+                             (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
+                             (x2:?) (subst1 d u t2 (lift (1) d x2)) ->
+                             (pc3 a x1 x2).
+      Intros; Pc3Confluence; Repeat Pr3GenContext.
+      Subst1Confluence; Rewrite H in H3; Clear H x3; XEAuto.
+      Qed.
+
+   End pc3_gen_context.