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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma
index ceb02c249..7acdf612f 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma
@@ -75,8 +75,7 @@ theorem s_le:
 \def
  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
 nat).((le i j) \to (le (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i: 
-nat).(\lambda (j: nat).(\lambda (H: (le i j)).(le_S_n (S i) (S j) (lt_le_S (S 
-i) (S (S j)) (lt_n_S i (S j) (le_lt_n_Sm i j H)))))))) (\lambda (_: 
+nat).(\lambda (j: nat).(\lambda (H: (le i j)).(le_n_S i j H))))) (\lambda (_: 
 F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (le i j)).H)))) k).
 
 theorem s_lt:
@@ -85,9 +84,8 @@ theorem s_lt:
 \def
  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
 nat).((lt i j) \to (lt (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i: 
-nat).(\lambda (j: nat).(\lambda (H: (lt i j)).(le_S_n (S (S i)) (S j) (le_n_S 
-(S (S i)) (S j) (le_n_S (S i) j H))))))) (\lambda (_: F).(\lambda (i: 
-nat).(\lambda (j: nat).(\lambda (H: (lt i j)).H)))) k).
+nat).(\lambda (j: nat).(\lambda (H: (lt i j)).(le_n_S (S i) j H))))) (\lambda 
+(_: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt i j)).H)))) k).
 
 theorem s_inj:
  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((eq nat (s k i) (s k j))