X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsubst0%2Fprops.ma;h=7b147c20e6a9d129d8e3d192c78e03b450fc9933;hb=b58315ef220a130a44acbf528cd6885ddadad642;hp=87dac12957c0f40aadddf5baa3859816a1129b73;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
index 87dac1295..7b147c20e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma
@@ -145,9 +145,9 @@ h d u1) (lift h (s k d) t0)) t)) (subst0_both (lift h (minus d (S i0)) v)
 (lift h d u1) (lift h d u2) i0 (H1 d H4 h) k (lift h (s k d) t0) (lift h (s k 
 d) t3) (eq_ind nat (minus (s k d) (s k (S i0))) (\lambda (n: nat).(subst0 (s 
 k i0) (lift h n v) (lift h (s k d) t0) (lift h (s k d) t3))) (H5 (s k d) 
-(lt_le_S (s k i0) (s k d) (s_lt k i0 d H4)) h) (minus d (S i0)) (minus_s_s k 
-d (S i0)))) (lift h d (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d 
-(THead k u1 t0)) (lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
+(s_lt k i0 d H4) h) (minus d (S i0)) (minus_s_s k d (S i0)))) (lift h d 
+(THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead k u1 t0)) 
+(lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
 
 theorem subst0_lift_ge:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall