X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fspare.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fspare.ma;h=e77507354e21843f091751b9af7997559285cec5;hb=3b2361afb73203749541ad07e94648da6057ae67;hp=040ab8d46cdc5b215a5359641c59df5026b852e5;hpb=413007de240fefb28650bb5ba7940f46db656751;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma
index 040ab8d46..e77507354 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma
@@ -433,12 +433,12 @@ j)))))))
 H1) in (let H2 \def H_x in (ex_ind T (\lambda (u0: T).(eq T (TLRef j) (lift 
 (S i) O u0))) (lt i j) (\lambda (x: T).(\lambda (H3: (eq T (TLRef j) (lift (S 
 i) O x))).(let H_x0 \def (lift_gen_lref x O (S i) j H3) in (let H4 \def H_x0 
-in (or_ind (land (lt j O) (eq T x (TLRef j))) (land (le (plus O (S i)) j) (eq 
-T x (TLRef (minus j (S i))))) (lt i j) (\lambda (H5: (land (lt j O) (eq T x 
+in (or_ind (land (lt j O) (eq T x (TLRef j))) (land (le (S i) j) (eq T x 
+(TLRef (minus j (S i))))) (lt i j) (\lambda (H5: (land (lt j O) (eq T x 
 (TLRef j)))).(land_ind (lt j O) (eq T x (TLRef j)) (lt i j) (\lambda (H6: (lt 
 j O)).(\lambda (_: (eq T x (TLRef j))).(lt_x_O j H6 (lt i j)))) H5)) (\lambda 
-(H5: (land (le (plus O (S i)) j) (eq T x (TLRef (minus j (S i)))))).(land_ind 
-(le (plus O (S i)) j) (eq T x (TLRef (minus j (S i)))) (lt i j) (\lambda (H6: 
-(le (plus O (S i)) j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6)) 
-H5)) H4))))) H2))))))))).
+(H5: (land (le (S i) j) (eq T x (TLRef (minus j (S i)))))).(land_ind (le (S 
+i) j) (eq T x (TLRef (minus j (S i)))) (lt i j) (\lambda (H6: (le (S i) 
+j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6)) H5)) H4))))) 
+H2))))))))).