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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
index 41139d520..e0f2654ac 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
@@ -52,11 +52,10 @@ theorem next_plus_lt:
 g n) h))))
 \def
  \lambda (g: G).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall (n0: 
-nat).(lt n0 (next_plus g (next g n0) n)))) (\lambda (n: nat).(le_S_n (S n) 
-(next g n) (lt_le_S (S n) (S (next g n)) (lt_n_S n (next g n) (next_lt g 
-n))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 (next_plus g 
-(next g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next 
-g n0)) n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus 
-g (next g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus 
-g (next g n0) n)) (next_plus_next g (next g n0) n))))) h)).
+nat).(lt n0 (next_plus g (next g n0) n)))) (\lambda (n: nat).(next_lt g n)) 
+(\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 (next_plus g (next 
+g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next g n0)) 
+n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next 
+g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next 
+g n0) n)) (next_plus_next g (next g n0) n))))) h)).