X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Farity%2Fpr3.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Farity%2Fpr3.ma;h=67617b31a886855c049c37f67d68fc7f86519081;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;hp=eaedb44aa0da5687ff7d463dea93708e7403a329;hpb=783fbc6eb42d5db260d93d8d213a7d5c035e99e3;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma
index eaedb44aa..67617b31a 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/pr3".
 
 include "csuba/arity.ma".
 
@@ -72,31 +72,31 @@ u t2) \to (arity g c2 t2 a1))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda
 C).((wcpr0 (CHead c (Bind b) u) c2) \to (\forall (t2: T).((pr0 t t2) \to 
 (arity g c2 t2 a2))))))).(\lambda (c2: C).(\lambda (H5: (wcpr0 c 
 c2)).(\lambda (t2: T).(\lambda (H6: (pr0 (THead (Bind b) u t) t2)).(insert_eq 
-T (THead (Bind b) u t) (\lambda (t0: T).(pr0 t0 t2)) (arity g c2 t2 a2) 
-(\lambda (y: T).(\lambda (H7: (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda 
-(t3: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 t3 a2)))) (\lambda 
-(t0: T).(\lambda (H8: (eq T t0 (THead (Bind b) u t))).(let H9 \def (f_equal T 
-T (\lambda (e: T).e) t0 (THead (Bind b) u t) H8) in (eq_ind_r T (THead (Bind 
-b) u t) (\lambda (t3: T).(arity g c2 t3 a2)) (arity_bind g b H0 c2 u a1 (H2 
-c2 H5 u (pr0_refl u)) t a2 (H4 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H5 u u 
-(pr0_refl u) (Bind b)) t (pr0_refl t))) t0 H9)))) (\lambda (u1: T).(\lambda 
-(u2: T).(\lambda (H8: (pr0 u1 u2)).(\lambda (H9: (((eq T u1 (THead (Bind b) u 
-t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda 
-(H10: (pr0 t3 t4)).(\lambda (H11: (((eq T t3 (THead (Bind b) u t)) \to (arity 
-g c2 t4 a2)))).(\lambda (k: K).(\lambda (H12: (eq T (THead k u1 t3) (THead 
-(Bind b) u t))).(let H13 \def (f_equal T K (\lambda (e: T).(match e in T 
-return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) 
-\Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) (THead (Bind 
-b) u t) H12) in ((let H14 \def (f_equal T T (\lambda (e: T).(match e in T 
-return (\lambda (_: T).T) with [(TSort _) \Rightarrow u1 | (TLRef _) 
-\Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) (THead 
-(Bind b) u t) H12) in ((let H15 \def (f_equal T T (\lambda (e: T).(match e in 
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | (TLRef _) 
-\Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead 
-(Bind b) u t) H12) in (\lambda (H16: (eq T u1 u)).(\lambda (H17: (eq K k 
-(Bind b))).(eq_ind_r K (Bind b) (\lambda (k0: K).(arity g c2 (THead k0 u2 t4) 
-a2)) (let H18 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Bind b) u 
-t)) \to (arity g c2 t4 a2))) H11 t H15) in (let H19 \def (eq_ind T t3 
+T (THead (Bind b) u t) (\lambda (t0: T).(pr0 t0 t2)) (\lambda (_: T).(arity g 
+c2 t2 a2)) (\lambda (y: T).(\lambda (H7: (pr0 y t2)).(pr0_ind (\lambda (t0: 
+T).(\lambda (t3: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 t3 a2)))) 
+(\lambda (t0: T).(\lambda (H8: (eq T t0 (THead (Bind b) u t))).(let H9 \def 
+(f_equal T T (\lambda (e: T).e) t0 (THead (Bind b) u t) H8) in (eq_ind_r T 
+(THead (Bind b) u t) (\lambda (t3: T).(arity g c2 t3 a2)) (arity_bind g b H0 
+c2 u a1 (H2 c2 H5 u (pr0_refl u)) t a2 (H4 (CHead c2 (Bind b) u) (wcpr0_comp 
+c c2 H5 u u (pr0_refl u) (Bind b)) t (pr0_refl t))) t0 H9)))) (\lambda (u1: 
+T).(\lambda (u2: T).(\lambda (H8: (pr0 u1 u2)).(\lambda (H9: (((eq T u1 
+(THead (Bind b) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda 
+(t4: T).(\lambda (H10: (pr0 t3 t4)).(\lambda (H11: (((eq T t3 (THead (Bind b) 
+u t)) \to (arity g c2 t4 a2)))).(\lambda (k: K).(\lambda (H12: (eq T (THead k 
+u1 t3) (THead (Bind b) u t))).(let H13 \def (f_equal T K (\lambda (e: 
+T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | 
+(TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) 
+(THead (Bind b) u t) H12) in ((let H14 \def (f_equal T T (\lambda (e: 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u1 | 
+(TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) 
+(THead (Bind b) u t) H12) in ((let H15 \def (f_equal T T (\lambda (e: 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | 
+(TLRef _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) 
+(THead (Bind b) u t) H12) in (\lambda (H16: (eq T u1 u)).(\lambda (H17: (eq K 
+k (Bind b))).(eq_ind_r K (Bind b) (\lambda (k0: K).(arity g c2 (THead k0 u2 
+t4) a2)) (let H18 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Bind 
+b) u t)) \to (arity g c2 t4 a2))) H11 t H15) in (let H19 \def (eq_ind T t3 
 (\lambda (t0: T).(pr0 t0 t4)) H10 t H15) in (let H20 \def (eq_ind T u1 
 (\lambda (t0: T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 u2 a2))) H9 
 u H16) in (let H21 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H8 u H16) 
@@ -212,14 +212,14 @@ C).((wcpr0 (CHead c (Bind Abst) u) c2) \to (\forall (t2: T).((pr0 t t2) \to
 (arity g c2 t2 a2))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c 
 c2)).(\lambda (t2: T).(\lambda (H5: (pr0 (THead (Bind Abst) u t) 
 t2)).(insert_eq T (THead (Bind Abst) u t) (\lambda (t0: T).(pr0 t0 t2)) 
-(arity g c2 t2 (AHead a1 a2)) (\lambda (y: T).(\lambda (H6: (pr0 y 
-t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq T t0 (THead (Bind Abst) 
-u t)) \to (arity g c2 t3 (AHead a1 a2))))) (\lambda (t0: T).(\lambda (H7: (eq 
-T t0 (THead (Bind Abst) u t))).(let H8 \def (f_equal T T (\lambda (e: T).e) 
-t0 (THead (Bind Abst) u t) H7) in (eq_ind_r T (THead (Bind Abst) u t) 
-(\lambda (t3: T).(arity g c2 t3 (AHead a1 a2))) (arity_head g c2 u a1 (H1 c2 
-H4 u (pr0_refl u)) t a2 (H3 (CHead c2 (Bind Abst) u) (wcpr0_comp c c2 H4 u u 
-(pr0_refl u) (Bind Abst)) t (pr0_refl t))) t0 H8)))) (\lambda (u1: 
+(\lambda (_: T).(arity g c2 t2 (AHead a1 a2))) (\lambda (y: T).(\lambda (H6: 
+(pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq T t0 (THead (Bind 
+Abst) u t)) \to (arity g c2 t3 (AHead a1 a2))))) (\lambda (t0: T).(\lambda 
+(H7: (eq T t0 (THead (Bind Abst) u t))).(let H8 \def (f_equal T T (\lambda 
+(e: T).e) t0 (THead (Bind Abst) u t) H7) in (eq_ind_r T (THead (Bind Abst) u 
+t) (\lambda (t3: T).(arity g c2 t3 (AHead a1 a2))) (arity_head g c2 u a1 (H1 
+c2 H4 u (pr0_refl u)) t a2 (H3 (CHead c2 (Bind Abst) u) (wcpr0_comp c c2 H4 u 
+u (pr0_refl u) (Bind Abst)) t (pr0_refl t))) t0 H8)))) (\lambda (u1: 
 T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 
 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 a2))))).(\lambda (t3: 
 T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 
@@ -332,75 +332,75 @@ C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda
 \to (\forall (t2: T).((pr0 t t2) \to (arity g c2 t2 (AHead a1 
 a2)))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t2: 
 T).(\lambda (H5: (pr0 (THead (Flat Appl) u t) t2)).(insert_eq T (THead (Flat 
-Appl) u t) (\lambda (t0: T).(pr0 t0 t2)) (arity g c2 t2 a2) (\lambda (y: 
-T).(\lambda (H6: (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq 
-T t0 (THead (Flat Appl) u t)) \to (arity g c2 t3 a2)))) (\lambda (t0: 
-T).(\lambda (H7: (eq T t0 (THead (Flat Appl) u t))).(let H8 \def (f_equal T T 
-(\lambda (e: T).e) t0 (THead (Flat Appl) u t) H7) in (eq_ind_r T (THead (Flat 
-Appl) u t) (\lambda (t3: T).(arity g c2 t3 a2)) (arity_appl g c2 u a1 (H1 c2 
-H4 u (pr0_refl u)) t a2 (H3 c2 H4 t (pr0_refl t))) t0 H8)))) (\lambda (u1: 
-T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 
-(THead (Flat Appl) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda 
-(t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat 
-Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (k: K).(\lambda (H11: (eq T 
-(THead k u1 t3) (THead (Flat Appl) u t))).(let H12 \def (f_equal T K (\lambda 
-(e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k 
-| (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) 
+Appl) u t) (\lambda (t0: T).(pr0 t0 t2)) (\lambda (_: T).(arity g c2 t2 a2)) 
+(\lambda (y: T).(\lambda (H6: (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda 
+(t3: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g c2 t3 a2)))) (\lambda 
+(t0: T).(\lambda (H7: (eq T t0 (THead (Flat Appl) u t))).(let H8 \def 
+(f_equal T T (\lambda (e: T).e) t0 (THead (Flat Appl) u t) H7) in (eq_ind_r T 
+(THead (Flat Appl) u t) (\lambda (t3: T).(arity g c2 t3 a2)) (arity_appl g c2 
+u a1 (H1 c2 H4 u (pr0_refl u)) t a2 (H3 c2 H4 t (pr0_refl t))) t0 H8)))) 
+(\lambda (u1: T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: 
+(((eq T u1 (THead (Flat Appl) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 
+(THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (k: K).(\lambda 
+(H11: (eq T (THead k u1 t3) (THead (Flat Appl) u t))).(let H12 \def (f_equal 
+T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) 
+\Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) 
+(THead k u1 t3) (THead (Flat Appl) u t) H11) in ((let H13 \def (f_equal T T 
+(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
+\Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) 
+(THead k u1 t3) (THead (Flat Appl) u t) H11) in ((let H14 \def (f_equal T T 
+(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
+\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) 
+(THead k u1 t3) (THead (Flat Appl) u t) H11) in (\lambda (H15: (eq T u1 
+u)).(\lambda (H16: (eq K k (Flat Appl))).(eq_ind_r K (Flat Appl) (\lambda 
+(k0: K).(arity g c2 (THead k0 u2 t4) a2)) (let H17 \def (eq_ind T t3 (\lambda 
+(t0: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2))) H10 t 
+H14) in (let H18 \def (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H9 t H14) in 
+(let H19 \def (eq_ind T u1 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u 
+t)) \to (arity g c2 u2 a2))) H8 u H15) in (let H20 \def (eq_ind T u1 (\lambda 
+(t0: T).(pr0 t0 u2)) H7 u H15) in (arity_appl g c2 u2 a1 (H1 c2 H4 u2 H20) t4 
+a2 (H3 c2 H4 t4 H18)))))) k H16)))) H13)) H12)))))))))))) (\lambda (u0: 
+T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H7: (pr0 v1 v2)).(\lambda (H8: 
+(((eq T v1 (THead (Flat Appl) u t)) \to (arity g c2 v2 a2)))).(\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 
+(THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (H11: (eq T 
+(THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Flat Appl) u 
+t))).(let H12 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda 
+(_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 | (THead 
+_ t0 _) \Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) 
 (THead (Flat Appl) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u1 | 
-(TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) 
-(THead (Flat Appl) u t) H11) in ((let H14 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | 
-(TLRef _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) 
-(THead (Flat Appl) u t) H11) in (\lambda (H15: (eq T u1 u)).(\lambda (H16: 
-(eq K k (Flat Appl))).(eq_ind_r K (Flat Appl) (\lambda (k0: K).(arity g c2 
-(THead k0 u2 t4) a2)) (let H17 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 
-(THead (Flat Appl) u t)) \to (arity g c2 t4 a2))) H10 t H14) in (let H18 \def 
-(eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind 
-T u1 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g c2 u2 
-a2))) H8 u H15) in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) 
-H7 u H15) in (arity_appl g c2 u2 a1 (H1 c2 H4 u2 H20) t4 a2 (H3 c2 H4 t4 
-H18)))))) k H16)))) H13)) H12)))))))))))) (\lambda (u0: T).(\lambda (v1: 
-T).(\lambda (v2: T).(\lambda (H7: (pr0 v1 v2)).(\lambda (H8: (((eq T v1 
-(THead (Flat Appl) u t)) \to (arity g c2 v2 a2)))).(\lambda (t3: T).(\lambda 
-(t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat 
-Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (H11: (eq T (THead (Flat Appl) 
-v1 (THead (Bind Abst) u0 t3)) (THead (Flat Appl) u t))).(let H12 \def 
-(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
-[(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 | (THead _ t0 _) 
-\Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead 
-(Flat Appl) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e 
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead (Bind Abst) 
-u0 t3) | (TLRef _) \Rightarrow (THead (Bind Abst) u0 t3) | (THead _ _ t0) 
-\Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead 
-(Flat Appl) u t) H11) in (\lambda (H14: (eq T v1 u)).(let H15 \def (eq_ind T 
-v1 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g c2 v2 
-a2))) H8 u H14) in (let H16 \def (eq_ind T v1 (\lambda (t0: T).(pr0 t0 v2)) 
-H7 u H14) in (let H17 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead 
-(Flat Appl) u t0)) \to (arity g c2 t4 a2))) H10 (THead (Bind Abst) u0 t3) 
-H13) in (let H18 \def (eq_ind_r T t (\lambda (t0: T).((eq T u (THead (Flat 
-Appl) u t0)) \to (arity g c2 v2 a2))) H15 (THead (Bind Abst) u0 t3) H13) in 
-(let H19 \def (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0 c c3) 
-\to (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 t5 (AHead a1 a2))))))) H3 
-(THead (Bind Abst) u0 t3) H13) in (let H20 \def (eq_ind_r T t (\lambda (t0: 
-T).(arity g c t0 (AHead a1 a2))) H2 (THead (Bind Abst) u0 t3) H13) in (let 
-H21 \def (H1 c2 H4 v2 H16) in (let H22 \def (H19 c2 H4 (THead (Bind Abst) u0 
-t4) (pr0_comp u0 u0 (pr0_refl u0) t3 t4 H9 (Bind Abst))) in (let H23 \def 
-(arity_gen_abst g c2 u0 t4 (AHead a1 a2) H22) in (ex3_2_ind A A (\lambda (a3: 
-A).(\lambda (a4: A).(eq A (AHead a1 a2) (AHead a3 a4)))) (\lambda (a3: 
-A).(\lambda (_: A).(arity g c2 u0 (asucc g a3)))) (\lambda (_: A).(\lambda 
-(a4: A).(arity g (CHead c2 (Bind Abst) u0) t4 a4))) (arity g c2 (THead (Bind 
-Abbr) v2 t4) a2) (\lambda (x0: A).(\lambda (x1: A).(\lambda (H24: (eq A 
-(AHead a1 a2) (AHead x0 x1))).(\lambda (H25: (arity g c2 u0 (asucc g 
-x0))).(\lambda (H26: (arity g (CHead c2 (Bind Abst) u0) t4 x1)).(let H27 \def 
-(f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) with 
-[(ASort _ _) \Rightarrow a1 | (AHead a0 _) \Rightarrow a0])) (AHead a1 a2) 
-(AHead x0 x1) H24) in ((let H28 \def (f_equal A A (\lambda (e: A).(match e in 
-A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a2 | (AHead _ a0) 
-\Rightarrow a0])) (AHead a1 a2) (AHead x0 x1) H24) in (\lambda (H29: (eq A a1 
-x0)).(let H30 \def (eq_ind_r A x1 (\lambda (a0: A).(arity g (CHead c2 (Bind 
-Abst) u0) t4 a0)) H26 a2 H28) in (let H31 \def (eq_ind_r A x0 (\lambda (a0: 
-A).(arity g c2 u0 (asucc g a0))) H25 a1 H29) in (arity_bind g Abbr 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead 
+(Bind Abst) u0 t3) | (TLRef _) \Rightarrow (THead (Bind Abst) u0 t3) | (THead 
+_ _ t0) \Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) 
+(THead (Flat Appl) u t) H11) in (\lambda (H14: (eq T v1 u)).(let H15 \def 
+(eq_ind T v1 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g 
+c2 v2 a2))) H8 u H14) in (let H16 \def (eq_ind T v1 (\lambda (t0: T).(pr0 t0 
+v2)) H7 u H14) in (let H17 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 
+(THead (Flat Appl) u t0)) \to (arity g c2 t4 a2))) H10 (THead (Bind Abst) u0 
+t3) H13) in (let H18 \def (eq_ind_r T t (\lambda (t0: T).((eq T u (THead 
+(Flat Appl) u t0)) \to (arity g c2 v2 a2))) H15 (THead (Bind Abst) u0 t3) 
+H13) in (let H19 \def (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0 
+c c3) \to (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 t5 (AHead a1 
+a2))))))) H3 (THead (Bind Abst) u0 t3) H13) in (let H20 \def (eq_ind_r T t 
+(\lambda (t0: T).(arity g c t0 (AHead a1 a2))) H2 (THead (Bind Abst) u0 t3) 
+H13) in (let H21 \def (H1 c2 H4 v2 H16) in (let H22 \def (H19 c2 H4 (THead 
+(Bind Abst) u0 t4) (pr0_comp u0 u0 (pr0_refl u0) t3 t4 H9 (Bind Abst))) in 
+(let H23 \def (arity_gen_abst g c2 u0 t4 (AHead a1 a2) H22) in (ex3_2_ind A A 
+(\lambda (a3: A).(\lambda (a4: A).(eq A (AHead a1 a2) (AHead a3 a4)))) 
+(\lambda (a3: A).(\lambda (_: A).(arity g c2 u0 (asucc g a3)))) (\lambda (_: 
+A).(\lambda (a4: A).(arity g (CHead c2 (Bind Abst) u0) t4 a4))) (arity g c2 
+(THead (Bind Abbr) v2 t4) a2) (\lambda (x0: A).(\lambda (x1: A).(\lambda 
+(H24: (eq A (AHead a1 a2) (AHead x0 x1))).(\lambda (H25: (arity g c2 u0 
+(asucc g x0))).(\lambda (H26: (arity g (CHead c2 (Bind Abst) u0) t4 x1)).(let 
+H27 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A) 
+with [(ASort _ _) \Rightarrow a1 | (AHead a0 _) \Rightarrow a0])) (AHead a1 
+a2) (AHead x0 x1) H24) in ((let H28 \def (f_equal A A (\lambda (e: A).(match 
+e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a2 | (AHead _ 
+a0) \Rightarrow a0])) (AHead a1 a2) (AHead x0 x1) H24) in (\lambda (H29: (eq 
+A a1 x0)).(let H30 \def (eq_ind_r A x1 (\lambda (a0: A).(arity g (CHead c2 
+(Bind Abst) u0) t4 a0)) H26 a2 H28) in (let H31 \def (eq_ind_r A x0 (\lambda 
+(a0: A).(arity g c2 u0 (asucc g a0))) H25 a1 H29) in (arity_bind g Abbr 
 not_abbr_abst c2 v2 a1 H21 t4 a2 (csuba_arity g (CHead c2 (Bind Abst) u0) t4 
 a2 H30 (CHead c2 (Bind Abbr) v2) (csuba_abst g c2 c2 (csuba_refl g c2) u0 a1 
 H31 v2 H21))))))) H27))))))) H23)))))))))))) H12)))))))))))) (\lambda (b: 
@@ -478,30 +478,30 @@ T).(\lambda (_: (arity g c t a0)).(\lambda (H3: ((\forall (c2: C).((wcpr0 c
 c2) \to (\forall (t2: T).((pr0 t t2) \to (arity g c2 t2 a0))))))).(\lambda 
 (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t2: T).(\lambda (H5: (pr0 
 (THead (Flat Cast) u t) t2)).(insert_eq T (THead (Flat Cast) u t) (\lambda 
-(t0: T).(pr0 t0 t2)) (arity g c2 t2 a0) (\lambda (y: T).(\lambda (H6: (pr0 y 
-t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq T t0 (THead (Flat Cast) 
-u t)) \to (arity g c2 t3 a0)))) (\lambda (t0: T).(\lambda (H7: (eq T t0 
-(THead (Flat Cast) u t))).(let H8 \def (f_equal T T (\lambda (e: T).e) t0 
-(THead (Flat Cast) u t) H7) in (eq_ind_r T (THead (Flat Cast) u t) (\lambda 
-(t3: T).(arity g c2 t3 a0)) (arity_cast g c2 u a0 (H1 c2 H4 u (pr0_refl u)) t 
-(H3 c2 H4 t (pr0_refl t))) t0 H8)))) (\lambda (u1: T).(\lambda (u2: 
-T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 (THead (Flat Cast) u 
-t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: 
-(pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat Cast) u t)) \to (arity g 
-c2 t4 a0)))).(\lambda (k: K).(\lambda (H11: (eq T (THead k u1 t3) (THead 
-(Flat Cast) u t))).(let H12 \def (f_equal T K (\lambda (e: T).(match e in T 
-return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) 
-\Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) (THead (Flat 
-Cast) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e in T 
-return (\lambda (_: T).T) with [(TSort _) \Rightarrow u1 | (TLRef _) 
-\Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) (THead 
-(Flat Cast) u t) H11) in ((let H14 \def (f_equal T T (\lambda (e: T).(match e 
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | (TLRef _) 
-\Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) (THead 
-(Flat Cast) u t) H11) in (\lambda (H15: (eq T u1 u)).(\lambda (H16: (eq K k 
-(Flat Cast))).(eq_ind_r K (Flat Cast) (\lambda (k0: K).(arity g c2 (THead k0 
-u2 t4) a0)) (let H17 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead 
-(Flat Cast) u t)) \to (arity g c2 t4 a0))) H10 t H14) in (let H18 \def 
+(t0: T).(pr0 t0 t2)) (\lambda (_: T).(arity g c2 t2 a0)) (\lambda (y: 
+T).(\lambda (H6: (pr0 y t2)).(pr0_ind (\lambda (t0: T).(\lambda (t3: T).((eq 
+T t0 (THead (Flat Cast) u t)) \to (arity g c2 t3 a0)))) (\lambda (t0: 
+T).(\lambda (H7: (eq T t0 (THead (Flat Cast) u t))).(let H8 \def (f_equal T T 
+(\lambda (e: T).e) t0 (THead (Flat Cast) u t) H7) in (eq_ind_r T (THead (Flat 
+Cast) u t) (\lambda (t3: T).(arity g c2 t3 a0)) (arity_cast g c2 u a0 (H1 c2 
+H4 u (pr0_refl u)) t (H3 c2 H4 t (pr0_refl t))) t0 H8)))) (\lambda (u1: 
+T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1 
+(THead (Flat Cast) u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda 
+(t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Flat 
+Cast) u t)) \to (arity g c2 t4 a0)))).(\lambda (k: K).(\lambda (H11: (eq T 
+(THead k u1 t3) (THead (Flat Cast) u t))).(let H12 \def (f_equal T K (\lambda 
+(e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k 
+| (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) 
+(THead (Flat Cast) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u1 | 
+(TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) 
+(THead (Flat Cast) u t) H11) in ((let H14 \def (f_equal T T (\lambda (e: 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | 
+(TLRef _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead k u1 t3) 
+(THead (Flat Cast) u t) H11) in (\lambda (H15: (eq T u1 u)).(\lambda (H16: 
+(eq K k (Flat Cast))).(eq_ind_r K (Flat Cast) (\lambda (k0: K).(arity g c2 
+(THead k0 u2 t4) a0)) (let H17 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 
+(THead (Flat Cast) u t)) \to (arity g c2 t4 a0))) H10 t H14) in (let H18 \def 
 (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H9 t H14) in (let H19 \def (eq_ind 
 T u1 (\lambda (t0: T).((eq T t0 (THead (Flat Cast) u t)) \to (arity g c2 u2 
 a0))) H8 u H15) in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2))