X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Faplus%2Fprops.ma;h=e0b2bcacae8bc68e28a9d8a115930abc9e59a534;hb=d0982534aee06a30f91a06d2f3e82834b132a3d3;hp=4df511966eb9dc6d202f2955793f9ade306d617b;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma
index 4df511966..e0b2bcaca 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma
@@ -14,8 +14,6 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/props".
-
 include "aplus/defs.ma".
 
 include "next_plus/props.ma".
@@ -29,12 +27,8 @@ theorem aplus_reg_r:
 (h2: nat).(\lambda (H: (eq A (aplus g a1 h1) (aplus g a2 h2))).(\lambda (h: 
 nat).(nat_ind (\lambda (n: nat).(eq A (aplus g a1 (plus n h1)) (aplus g a2 
 (plus n h2)))) H (\lambda (n: nat).(\lambda (H0: (eq A (aplus g a1 (plus n 
-h1)) (aplus g a2 (plus n h2)))).(sym_eq A (asucc g (aplus g a2 (plus n h2))) 
-(asucc g (aplus g a1 (plus n h1))) (sym_eq A (asucc g (aplus g a1 (plus n 
-h1))) (asucc g (aplus g a2 (plus n h2))) (sym_eq A (asucc g (aplus g a2 (plus 
-n h2))) (asucc g (aplus g a1 (plus n h1))) (f_equal2 G A A asucc g g (aplus g 
-a2 (plus n h2)) (aplus g a1 (plus n h1)) (refl_equal G g) (sym_eq A (aplus g 
-a1 (plus n h1)) (aplus g a2 (plus n h2)) H0))))))) h))))))).
+h1)) (aplus g a2 (plus n h2)))).(f_equal2 G A A asucc g g (aplus g a1 (plus n 
+h1)) (aplus g a2 (plus n h2)) (refl_equal G g) H0))) h))))))).
 
 theorem aplus_assoc:
  \forall (g: G).(\forall (a: A).(\forall (h1: nat).(\forall (h2: nat).(eq A 
@@ -51,14 +45,9 @@ g a (plus n h2)))))).(\lambda (h2: nat).(nat_ind (\lambda (n0: nat).(eq A
 n)) (\lambda (n0: nat).(\lambda (H0: (eq A (aplus g (asucc g (aplus g a n)) 
 n0) (asucc g (aplus g a (plus n n0))))).(eq_ind nat (S (plus n n0)) (\lambda 
 (n1: nat).(eq A (asucc g (aplus g (asucc g (aplus g a n)) n0)) (asucc g 
-(aplus g a n1)))) (sym_eq A (asucc g (asucc g (aplus g a (plus n n0)))) 
-(asucc g (aplus g (asucc g (aplus g a n)) n0)) (sym_eq A (asucc g (aplus g 
-(asucc g (aplus g a n)) n0)) (asucc g (asucc g (aplus g a (plus n n0)))) 
-(sym_eq A (asucc g (asucc g (aplus g a (plus n n0)))) (asucc g (aplus g 
-(asucc g (aplus g a n)) n0)) (f_equal2 G A A asucc g g (asucc g (aplus g a 
-(plus n n0))) (aplus g (asucc g (aplus g a n)) n0) (refl_equal G g) (sym_eq A 
-(aplus g (asucc g (aplus g a n)) n0) (asucc g (aplus g a (plus n n0))) 
-H0))))) (plus n (S n0)) (plus_n_Sm n n0)))) h2)))) h1))).
+(aplus g a n1)))) (f_equal2 G A A asucc g g (aplus g (asucc g (aplus g a n)) 
+n0) (asucc g (aplus g a (plus n n0))) (refl_equal G g) H0) (plus n (S n0)) 
+(plus_n_Sm n n0)))) h2)))) h1))).
 
 theorem aplus_asucc:
  \forall (g: G).(\forall (h: nat).(\forall (a: A).(eq A (aplus g (asucc g a)