X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Farity%2Ffwd.ma;h=cba7ad939ee03ecd61f210c0b5406249ff870bbb;hb=20377cd037f6cc5eb9c6a5664354a8a0189d3f4f;hp=b0ca1a3b1921f73a8601d38449089ebd27d4daef;hpb=289d8d049e72beef41c17930f13727b5049981a2;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma
index b0ca1a3b1..cba7ad939 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma
@@ -663,15 +663,16 @@ A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda
 (asucc g x0))).(\lambda (H11: (arity g (CHead c0 (Bind Abst) u) t x1)).(let 
 H12 \def (eq_ind A a1 (\lambda (a0: A).(leq g a0 a2)) H3 (AHead x0 x1) H9) in 
 (let H13 \def (eq_ind A a1 (\lambda (a0: A).(arity g c0 (THead (Bind Abst) u 
-t) a0)) H7 (AHead x0 x1) H9) in (let H_x \def (leq_gen_head g x0 x1 a2 H12) 
-in (let H14 \def H_x in (ex3_2_ind A A (\lambda (a3: A).(\lambda (a4: A).(eq 
-A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: A).(leq g x0 a3))) 
-(\lambda (_: A).(\lambda (a4: A).(leq g x1 a4))) (ex3_2 A A (\lambda (a3: 
+t) a0)) H7 (AHead x0 x1) H9) in (let H_x \def (leq_gen_head1 g x0 x1 a2 H12) 
+in (let H14 \def H_x in (ex3_2_ind A A (\lambda (a3: A).(\lambda (_: A).(leq 
+g x0 a3))) (\lambda (_: A).(\lambda (a4: A).(leq g x1 a4))) (\lambda (a3: 
+A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (ex3_2 A A (\lambda (a3: 
 A).(\lambda (a4: A).(eq A a2 (AHead a3 a4)))) (\lambda (a3: A).(\lambda (_: 
 A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity g 
 (CHead c0 (Bind Abst) u) t a4)))) (\lambda (x2: A).(\lambda (x3: A).(\lambda 
-(H15: (eq A a2 (AHead x2 x3))).(\lambda (H16: (leq g x0 x2)).(\lambda (H17: 
-(leq g x1 x3)).(eq_ind_r A (AHead x2 x3) (\lambda (a0: A).(ex3_2 A A (\lambda 
+(H15: (leq g x0 x2)).(\lambda (H16: (leq g x1 x3)).(\lambda (H17: (eq A a2 
+(AHead x2 x3))).(let H18 \def (f_equal A A (\lambda (e: A).e) a2 (AHead x2 
+x3) H17) in (eq_ind_r A (AHead x2 x3) (\lambda (a0: A).(ex3_2 A A (\lambda 
 (a3: A).(\lambda (a4: A).(eq A a0 (AHead a3 a4)))) (\lambda (a3: A).(\lambda 
 (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda (a4: A).(arity 
 g (CHead c0 (Bind Abst) u) t a4))))) (ex3_2_intro A A (\lambda (a3: 
@@ -679,7 +680,7 @@ A).(\lambda (a4: A).(eq A (AHead x2 x3) (AHead a3 a4)))) (\lambda (a3:
 A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda 
 (a4: A).(arity g (CHead c0 (Bind Abst) u) t a4))) x2 x3 (refl_equal A (AHead 
 x2 x3)) (arity_repl g c0 u (asucc g x0) H10 (asucc g x2) (asucc_repl g x0 x2 
-H16)) (arity_repl g (CHead c0 (Bind Abst) u) t x1 H11 x3 H17)) a2 H15)))))) 
+H15)) (arity_repl g (CHead c0 (Bind Abst) u) t x1 H11 x3 H16)) a2 H18))))))) 
 H14)))))))))) H8))))))))))))) c y a H0))) H)))))).
 
 theorem arity_gen_appl: