we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
deleted file mode 100644 (file)
index b5fef20..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
+++ /dev/null
@@ -1,62 +0,0 @@
-(*#* #stop file *)
-
-Require tlt_defs.
-Require lift_tlt.
-Require subst0_defs.
-
-   Section subst0_tlt_props. (***********************************************)
-
-      Theorem subst0_weight_le : (u,t,z:?; d:?) (subst0 d u t z) ->
-                                 (f,g:?) ((m:?) (le (f m) (g m))) ->
-                                 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
-                                 (le (weight_map f z) (weight_map g t)).
-      Intros until 1; XElim H.
-(* case 1: subst0_lref *)
-      Intros; XAuto.
-(* case 2: subst0_fst *)
-      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
-(* case 3: subst0_snd *)
-      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
-(* case 4: subst0_both *)
-      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
-      Qed.
-
-      Theorem subst0_weight_lt : (u,t,z:?; d:?) (subst0 d u t z) -> (f,g:?)
-                                 ((m:?) (le (f m) (g m))) ->
-                                 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
-                                 (lt (weight_map f z) (weight_map g t)).
-      Intros until 1; XElim H.
-(* case 1: subst0_lref *)
-      Intros; XAuto.
-(* case 2: subst0_fst *)
-      XElim k; [ XElim b | Idtac ]; Simpl; Intros;
-      Apply lt_n_S; (Apply lt_le_plus_plus; [ XAuto | Idtac ]); (**)
-      [ Auto 6 with ltlc (**) | XAuto | XAuto | XAuto ].
-(* case 3: subst0_snd *)
-      XElim k; [ XElim b | Idtac ]; Simpl;
-      [ Auto 8 with ltlc | Auto 6 with ltlc | Auto 6 with ltlc | XAuto ]. (**)
-(* case 3: subst0_both *)
-      XElim k; [ XElim b | Idtac ]; Simpl;
-      Intros; Apply lt_n_S; [ Apply lt_le_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus ]; XAuto.
-      EApply subst0_weight_le; [ XEAuto | XAuto | XAuto ].
-      Qed.
-
-      Theorem subst0_tlt_tail: (u,t,z:?) (subst0 (0) u t z) ->
-                               (tlt (TTail (Bind Abbr) u z)
-                                    (TTail (Bind Abbr) u t)
-                               ).
-      Unfold tlt weight; Intros; Simpl.
-      Apply lt_n_S; Apply le_lt_plus_plus; [ XAuto | Idtac ].
-      EApply subst0_weight_lt; [ XEAuto | XAuto | XAuto ].
-      Qed.
-
-      Theorem subst0_tlt: (u,t,z:?) (subst0 (0) u t z) ->
-                          (tlt z (TTail (Bind Abbr) u t)).
-      Intros.
-      EApply tlt_trans; [ Idtac | Apply subst0_tlt_tail; XEAuto].
-      XAuto.
-      Qed.
-
-   End subst0_tlt_props.
-
-      Hints Resolve subst0_tlt : ltlc.