we restored the scripts of \lambda\delta version 1

[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
deleted file mode 100644 (file)
index 42f03f2..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen_context.v
+++ /dev/null
@@ -1,22 +0,0 @@
-(*#* #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; Pc3Unfold; Repeat Pr3GenContext.
-      Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XEAuto.
-      Qed.
-
-   End pc3_gen_context.