cicNotationPp: fixed letin syntax (now typeless)

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / spare.ma

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 040ab8d46cdc5b215a5359641c59df5026b852e5..e77507354e21843f091751b9af7997559285cec5 100644 (file)
--- 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))))))))).