we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
deleted file mode 100644 (file)
index 3546cb5..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
+++ /dev/null
@@ -1,33 +0,0 @@
-(*#* #stop file *)
-
-Require subst0_lift.
-Require drop_props.
-Require pr0_lift.
-Require pr2_defs.
-
-(*#* #caption "main properties of predicate \\texttt{pr2}" *)
-(*#* #clauses pr2_props *)
-
-   Section pr2_lift. (*******************************************************)
-
-(*#* #caption "conguence with lift" *)
-(*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
-
-      Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) ->
-                         (t1,t2:?) (pr2 e t1 t2) ->
-                         (pr2 c (lift h d t1) (lift h d t2)).
-      Intros until 2; XElim H0; Intros.
-(* case 1 : pr2_free *)
-      XAuto.
-(* case 2 : pr2_delta *)
-      Apply (lt_le_e i d); Intros; DropDis.
-(* case 2.1 : i < d *)
-      Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
-      DropGenBase; Rewrite H0 in H; Simpl in H; XEAuto.
-(* case 2.2 : i >= d *)
-      XEAuto.
-      Qed.
-
-   End pr2_lift.
-
-      Hints Resolve pr2_lift : ltlc.