we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v b/helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v
deleted file mode 100644 (file)
index 3967571..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v
+++ /dev/null
@@ -1,23 +0,0 @@
-(*#* #stop file *)
-
-Require lift_props.
-Require subst0_lift.
-Require subst1_defs.
-
-   Section subst1_lift. (****************************************************)
-
-      Theorem subst1_lift_lt : (t1,t2,u:?; i:?) (subst1 i u t1 t2) ->
-                               (d:?) (lt i d) -> (h:?)
-                               (subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
-      Intros until 1; XElim H; Clear t2; XAuto.
-      Qed.
-
-      Theorem subst1_lift_ge : (t1,t2,u:?; i,h:?) (subst1 i u t1 t2) ->
-                               (d:?) (le d i) ->
-                               (subst1 (plus i h) u (lift h d t1) (lift h d t2)).
-      Intros until 1; XElim H; Clear t2; XAuto.
-      Qed.
-
-   End subst1_lift.
-
-      Hints Resolve subst1_lift_lt subst1_lift_ge : ltlc.