X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FBase%2Fext%2Farith.ma;h=2ebbe44de123451605a5c03a5dfb9ea53dd2aa8c;hb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;hp=fc33cc52994649cb0e2cc37427fd0e0fbe74492c;hpb=884ac867259b5303a8f6c64faaf1591bd96a264e;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma
index fc33cc529..2ebbe44de 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma
@@ -189,9 +189,10 @@ theorem minus_le:
 \def
  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n 
 y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall 
-(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(match y in nat return 
-(\lambda (n0: nat).(le (minus (S n) n0) (S n))) with [O \Rightarrow (le_n (S 
-n)) | (S n0) \Rightarrow (le_S (minus n n0) n (H n0))])))) x).
+(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda (n0: 
+nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: nat).(\lambda 
+(_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)]) 
+(S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
 
 theorem le_plus_minus_sym:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) 
@@ -529,8 +530,8 @@ nat).(nat_ind (\lambda (n: nat).(\forall (y1: nat).(\forall (y2: nat).((le O
 nat).(\forall (y3: nat).(\forall (y4: nat).((le O z0) \to ((le O z0) \to ((eq 
 nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) H_y z0 (minus_n_O z0)) 
 in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (H2 (plus z0 y2) (plus z0 y1) (le_O_n 
-z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1) 
-(sym_equal nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2) 
+z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1) (sym_eq 
+nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2) 
 H1)))))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall 
 (y2: nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) 
 (plus (match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)])