we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v
deleted file mode 100644 (file)
index caabbe0..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v
+++ /dev/null
@@ -1,56 +0,0 @@
-(*#* #stop file *)
-
-Require lift_props.
-Require subst0_defs.
-
-   Section subst0_lift. (****************************************************)
-
-      Theorem subst0_lift_lt: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
-                              (d:?) (lt i d) -> (h:?)
-                              (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
-       Intros until 1; XElim H; Intros.
-(* case 1: subst0_lref *)
-       Rewrite lift_lref_lt; [ Idtac | XAuto ].
-       LetTac w := (minus d (S i0)).
-       Arith8 d '(S i0); Rewrite lift_d; XAuto.
-(* case 2: subst0_fst *)
-       LiftTailRw; XAuto.
-(* case 3: subst0_snd *)
-       SRwBackIn H0; LiftTailRw; Rewrite <- (minus_s_s k); XAuto.
-(* case 4: subst0_both *)
-       SRwBackIn H2; LiftTailRw.
-       Apply subst0_both; [ Idtac | Rewrite <- (minus_s_s k) ]; XAuto.
-       Qed.
-
-      Theorem subst0_lift_ge: (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
-                              (d:?) (le d i) ->
-                              (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
-      Intros until 1; XElim H; Intros.
-(* case 1: subst0_lref *)
-      Rewrite lift_lref_ge; [ Idtac | XAuto ].
-      Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
-      Arith5'c h i0; XAuto.
-(* case 2: subst0_fst *)
-      LiftTailRw; XAuto.
-(* case 3: subst0_snd *)
-      SRwBackIn H0; LiftTailRw; XAuto.
-(* case 4: subst0_snd *)
-      SRwBackIn H2; LiftTailRw; XAuto.
-      Qed.
-
-      Theorem subst0_lift_ge_S: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
-                                (d:?) (le d i) ->
-                                (subst0 (S i) u (lift (1) d t1) (lift (1) d t2)).
-      Intros; Arith7 i; Apply subst0_lift_ge; XAuto.
-      Qed.
-
-      Theorem subst0_lift_ge_s: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
-                                (d:?) (le d i) -> (b:?)
-                                (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
-      Intros; Simpl; Apply subst0_lift_ge_S; XAuto.
-      Qed.
-
-   End subst0_lift.
-      
-      Hints Resolve subst0_lift_lt subst0_lift_ge 
-                    subst0_lift_ge_S subst0_lift_ge_s : ltlc.