we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
deleted file mode 100644 (file)
index b6d9ba2..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require lift_props.
-Require subst0_lift.
-Require pr0_defs.
-
-(*#* #caption "main properties of the relation $\\PrZ{}{}$" *)
-(*#* #clauses pr0_props *)
-
-(*#* #stop file *)
-
-   Section pr0_lift. (*******************************************************)
-
-(*#* #caption "conguence with lift" *)
-(*#* #cap #cap t1,t2 #alpha d in i *)
-
-      Theorem pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
-                        (h,d:?) (pr0 (lift h d t1) (lift h d t2)).
-
-      Intros until 1; XElim H; Intros.
-(* case 1: pr0_refl *)
-      XAuto.
-(* case 2: pr0_cong *)
-      LiftTailRw; XAuto.
-(* case 3 : pr0_beta *)
-      LiftTailRw; XAuto.
-(* case 4: pr0_upsilon *)
-      LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
-(* case 5: pr0_delta *)
-      LiftTailRw; Simpl.
-      EApply pr0_delta; [ XAuto | Apply H2 | Idtac ].
-      LetTac d' := (S d); Arith10 d; Unfold d'; XAuto.
-(* case 6: pr0_zeta *)
-      LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
-(* case 7: pr0_epsilon *)
-      LiftTailRw; XAuto.
-      Qed.
-
-   End pr0_lift.
-
-      Hints Resolve pr0_lift : ltlc.