we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v
deleted file mode 100644 (file)
index d99a405..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v
+++ /dev/null
@@ -1,62 +0,0 @@
-Require Export lift_defs.
-
-(*#* #caption "axioms for strict substitution in terms",
-   "substituted local reference",
-   "substituted tail item: first operand", 
-   "substituted tail item: second operand", 
-   "substituted tail item: both operands"
-*)
-(*#* #cap #cap t, t1, t2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, s in p *)
-
-      Inductive subst0 : nat -> T -> T -> T -> Prop :=
-         | subst0_lref: (v:?; i:?) (subst0 i v (TLRef i) (lift (S i) (0) v))
-         | subst0_fst : (v,u2,u1:?; i:?) (subst0 i v u1 u2) ->
-                        (t:?; k:?) (subst0 i v (TTail k u1 t) (TTail k u2 t))
-         | subst0_snd : (k:?; v,t2,t1:?; i:?) (subst0 (s k i) v t1 t2) -> (u:?)
-                        (subst0 i v (TTail k u t1) (TTail k u t2))
-         | subst0_both: (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
-                        (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
-                        (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
-
-(*#* #stop file *)
-
-      Hint subst0 : ltlc := Constructors subst0.
-
-   Section subst0_gen_base. (************************************************)
-
-      Theorem subst0_gen_sort : (v,x:?; i,n:?) (subst0 i v (TSort n) x) ->
-                                (P:Prop) P.
-      Intros; Inversion H.
-      Qed.
-
-      Theorem subst0_gen_lref : (v,x:?; i,n:?) (subst0 i v (TLRef n) x) ->
-                                n = i /\ x = (lift (S n) (0) v).
-      Intros; Inversion H; XAuto.
-      Qed.
-
-      Theorem subst0_gen_tail : (k:?; v,u1,t1,x:?; i:?)
-                                (subst0 i v (TTail k u1 t1) x) -> (OR
-                                (EX u2 | x = (TTail k u2 t1) &
-                                        (subst0 i v u1 u2)) |
-                                (EX t2 | x = (TTail k u1 t2) &
-                                         (subst0 (s k i) v t1 t2)) |
-                                (EX u2 t2 | x = (TTail k u2 t2) &
-                                            (subst0 i v u1 u2) &
-                                            (subst0 (s k i) v t1 t2))
-                                ).
-
-      Intros; Inversion H; XEAuto.
-      Qed.
-
-   End subst0_gen_base.
-
-      Tactic Definition Subst0GenBase :=
-         Match Context With
-            | [ H: (subst0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
-               Apply (subst0_gen_sort ?2 ?4 ?1 ?3); Apply H
-            | [ H: (subst0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
-               LApply (subst0_gen_lref ?2 ?4 ?1 ?3); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros
-            | [ H: (subst0 ?1 ?2 (TTail ?3 ?4 ?5) ?6) |- ? ] ->
-               LApply (subst0_gen_tail ?3 ?2 ?4 ?5 ?6 ?1); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros H; XElim H; Intros.