we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
deleted file mode 100644 (file)
index 93e0d2e..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
+++ /dev/null
@@ -1,58 +0,0 @@
-(*#* #stop file *)
-
-Require Export subst0_defs.
-
-      Inductive subst1 [i:nat; v:T; t1:T] : T -> Prop :=
-         | subst1_refl   : (subst1 i v t1 t1)
-         | subst1_single : (t2:?) (subst0 i v t1 t2) -> (subst1 i v t1 t2).
-
-      Hint subst1 : ltlc := Constructors subst1.
-
-   Section subst1_props. (***************************************************)
-
-      Theorem subst1_tail: (v,u1,u2:?; i:?) (subst1 i v u1 u2) ->
-                           (k:?; t1,t2:?) (subst1 (s k i) v t1 t2) ->
-                           (subst1 i v (TTail k u1 t1) (TTail k u2 t2)).
-      Intros until 1; XElim H; Clear u2.
-(* case 1: csubst1_refl *)
-      Intros until 1; XElim H; Clear t2; XAuto.
-(* case 2: csubst1_single *)
-      Intros until 2; XElim H0; Clear t3; XAuto.
-      Qed.
-
-   End subst1_props.
-
-      Hints Resolve subst1_tail : ltlc.
-
-   Section subst1_gen_base. (************************************************)
-
-      Theorem subst1_gen_sort : (v,x:?; i,n:?) (subst1 i v (TSort n) x) ->
-                                x = (TSort n).
-      Intros; XElim H; Clear x; Intros;
-      Try Subst0GenBase; XAuto.
-      Qed.
-
-      Theorem subst1_gen_lref : (v,x:?; i,n:?) (subst1 i v (TLRef n) x) ->
-                                x = (TLRef n) \/
-                                n = i /\ x = (lift (S n) (0) v).
-      Intros; XElim H; Clear x; Intros;
-      Try Subst0GenBase; XAuto.
-      Qed.
-
-      Theorem subst1_gen_tail : (k:?; v,u1,t1,x:?; i:?)
-                                (subst1 i v (TTail k u1 t1) x) ->
-                                (EX u2 t2 | x = (TTail k u2 t2) &
-                                            (subst1 i v u1 u2) &
-                                            (subst1 (s k i) v t1 t2)
-                                ).
-      Intros; XElim H; Clear x; Intros;
-      Try Subst0GenBase; XEAuto.
-      Qed.
-
-   End subst1_gen_base.
-
-      Tactic Definition Subst1GenBase :=
-         Match Context With
-            | [ H: (subst1 ?1 ?2 (TTail ?3 ?4 ?5) ?6) |- ? ] ->
-               LApply (subst1_gen_tail ?3 ?2 ?4 ?5 ?6 ?1); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros.