X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fsubst0_lift.v;h=caabbe0b7753f6be16e403d56e55c189768d01fb;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d4ce7412f56d8380635112ec93fa6250419573f5;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v
index d4ce7412f..caabbe0b7 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v
@@ -5,12 +5,12 @@ 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)).
+      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_bref *)
-       Rewrite lift_bref_lt; [ Idtac | XAuto ].
+(* 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 *)
@@ -22,12 +22,12 @@ Require subst0_defs.
        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)).
+      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_bref *)
-      Rewrite lift_bref_ge; [ Idtac | XAuto ].
+(* 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 *)
@@ -38,12 +38,19 @@ Require subst0_defs.
       SRwBackIn H2; LiftTailRw; 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; Arith7 i; Apply subst0_lift_ge; XAuto.
+      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.
 
-   End subst0_lift.
+      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.
 
-      Hints Resolve subst0_lift_lt subst0_lift_ge subst0_lift_ge_S : ltlc.
+   End subst0_lift.
+      
+      Hints Resolve subst0_lift_lt subst0_lift_ge 
+                    subst0_lift_ge_S subst0_lift_ge_s : ltlc.