X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fs%2Fprops.ma;h=f77a611e5a3659a3311873f6dc95ab696322f278;hb=5c1b44dfefa085fbb56e23047652d3650be9d855;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..f77a611e5 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
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/props".
+
 
 include "s/defs.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))