X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Farity%2Fpr3.ma;h=69dfef63d75f625ebd5793d4c7daab8a6fb45b5e;hp=f8952088ee20470060d56e69f6d2f49c20307b3e;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hpb=88a68a9c334646bc17314d5327cd3b790202acd6

diff --git a/matita/matita/contribs/lambdadelta/basic_1/arity/pr3.ma b/matita/matita/contribs/lambdadelta/basic_1/arity/pr3.ma
index f8952088e..69dfef63d 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/arity/pr3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/arity/pr3.ma
@@ -14,19 +14,19 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/csuba/arity.ma".
+include "basic_1/csuba/arity.ma".
 
-include "Basic-1/pr3/defs.ma".
+include "basic_1/pr3/fwd.ma".
 
-include "Basic-1/pr1/defs.ma".
+include "basic_1/pr1/fwd.ma".
 
-include "Basic-1/wcpr0/getl.ma".
+include "basic_1/wcpr0/getl.ma".
 
-include "Basic-1/pr0/fwd.ma".
+include "basic_1/pr0/props.ma".
 
-include "Basic-1/arity/subst0.ma".
+include "basic_1/arity/subst0.ma".
 
-theorem arity_sred_wcpr0_pr0:
+lemma arity_sred_wcpr0_pr0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (a: A).((arity g 
 c1 t1 a) \to (\forall (c2: C).((wcpr0 c1 c2) \to (\forall (t2: T).((pr0 t1 
 t2) \to (arity g c2 t2 a)))))))))
@@ -83,108 +83,93 @@ T).(\lambda (u2: T).(\lambda (H8: (pr0 u1 u2)).(\lambda (H9: (((eq T u1
 (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) 
+T).(match e 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 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 
+T).(match e 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) in (arity_bind g b H0 c2 
+u2 a1 (H2 c2 H5 u2 H21) t4 a2 (H4 (CHead c2 (Bind b) u2) (wcpr0_comp c c2 H5 
+u u2 H21 (Bind b)) t4 H19)))))) k H17)))) H14)) H13)))))))))))) (\lambda (u0: 
+T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: 
+(((eq T v1 (THead (Bind b) u t)) \to (arity g c2 v2 a2)))).(\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead 
+(Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (H12: (eq T (THead (Flat 
+Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Bind b) u t))).(let H13 \def 
+(eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: 
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
+| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat 
+_) \Rightarrow True])])) I (THead (Bind b) u t) H12) in (False_ind (arity g 
+c2 (THead (Bind Abbr) v2 t4) a2) H13)))))))))))) (\lambda (b0: B).(\lambda 
+(_: (not (eq B b0 Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 
+v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u t)) \to (arity g c2 v2 
+a2)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda 
+(_: (((eq T u1 (THead (Bind b) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead 
+(Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (H15: (eq T (THead (Flat 
+Appl) v1 (THead (Bind b0) u1 t3)) (THead (Bind b) u t))).(let H16 \def 
+(eq_ind T (THead (Flat Appl) v1 (THead (Bind b0) u1 t3)) (\lambda (ee: 
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
+| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat 
+_) \Rightarrow True])])) I (THead (Bind b) u t) H15) in (False_ind (arity g 
+c2 (THead (Bind b0) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) a2) 
+H16))))))))))))))))) (\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 (w: 
+T).(\lambda (H12: (subst0 O u2 t4 w)).(\lambda (H13: (eq T (THead (Bind Abbr) 
+u1 t3) (THead (Bind b) u t))).(let H14 \def (f_equal T B (\lambda (e: 
+T).(match e with [(TSort _) \Rightarrow Abbr | (TLRef _) \Rightarrow Abbr | 
+(THead k _ _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) 
+\Rightarrow Abbr])])) (THead (Bind Abbr) u1 t3) (THead (Bind b) u t) H13) in 
+((let H15 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
+\Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t0 _) \Rightarrow t0])) 
+(THead (Bind Abbr) u1 t3) (THead (Bind b) u t) H13) in ((let H16 \def 
+(f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t3 | (TLRef 
+_) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abbr) u1 
+t3) (THead (Bind b) u t) H13) in (\lambda (H17: (eq T u1 u)).(\lambda (H18: 
+(eq B Abbr b)).(let H19 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead 
+(Bind b) u t)) \to (arity g c2 t4 a2))) H11 t H16) in (let H20 \def (eq_ind T 
+t3 (\lambda (t0: T).(pr0 t0 t4)) H10 t H16) in (let H21 \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) 
-in (arity_bind g b H0 c2 u2 a1 (H2 c2 H5 u2 H21) t4 a2 (H4 (CHead c2 (Bind b) 
-u2) (wcpr0_comp c c2 H5 u u2 H21 (Bind b)) t4 H19)))))) k H17)))) H14)) 
-H13)))))))))))) (\lambda (u0: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda 
-(_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u t)) \to (arity g 
-c2 v2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 
-t4)).(\lambda (_: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 
-a2)))).(\lambda (H12: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) 
-(THead (Bind b) u t))).(let H13 \def (eq_ind T (THead (Flat Appl) v1 (THead 
-(Bind Abst) u0 t3)) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
-(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
-[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind 
-b) u t) H12) in (False_ind (arity g c2 (THead (Bind Abbr) v2 t4) a2) 
-H13)))))))))))) (\lambda (b0: B).(\lambda (_: (not (eq B b0 Abst))).(\lambda 
-(v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 
-(THead (Bind b) u t)) \to (arity g c2 v2 a2)))).(\lambda (u1: T).(\lambda 
-(u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead (Bind b) u 
-t)) \to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: 
-(pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 
-a2)))).(\lambda (H15: (eq T (THead (Flat Appl) v1 (THead (Bind b0) u1 t3)) 
-(THead (Bind b) u t))).(let H16 \def (eq_ind T (THead (Flat Appl) v1 (THead 
-(Bind b0) u1 t3)) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
-(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
-[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind 
-b) u t) H15) in (False_ind (arity g c2 (THead (Bind b0) u2 (THead (Flat Appl) 
-(lift (S O) O v2) t4)) a2) H16))))))))))))))))) (\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 (w: T).(\lambda (H12: (subst0 O u2 t4 w)).(\lambda 
-(H13: (eq T (THead (Bind Abbr) u1 t3) (THead (Bind b) u t))).(let H14 \def 
-(f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with 
-[(TSort _) \Rightarrow Abbr | (TLRef _) \Rightarrow Abbr | (THead k _ _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0) 
-\Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (THead (Bind Abbr) u1 t3) 
-(THead (Bind b) u t) H13) in ((let H15 \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 (Bind 
-Abbr) u1 t3) (THead (Bind b) u t) H13) in ((let H16 \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 (Bind Abbr) u1 t3) (THead (Bind b) u t) H13) in (\lambda (H17: (eq T 
-u1 u)).(\lambda (H18: (eq B Abbr b)).(let H19 \def (eq_ind T t3 (\lambda (t0: 
-T).((eq T t0 (THead (Bind b) u t)) \to (arity g c2 t4 a2))) H11 t H16) in 
-(let H20 \def (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H10 t H16) in (let 
-H21 \def (eq_ind T u1 (\lambda (t0: T).((eq T t0 (THead (Bind b) u t)) \to 
-(arity g c2 u2 a2))) H9 u H17) in (let H22 \def (eq_ind T u1 (\lambda (t0: 
-T).(pr0 t0 u2)) H8 u H17) in (let H23 \def (eq_ind_r B b (\lambda (b0: 
-B).((eq T t (THead (Bind b0) u t)) \to (arity g c2 t4 a2))) H19 Abbr H18) in 
-(let H24 \def (eq_ind_r B b (\lambda (b0: B).((eq T u (THead (Bind b0) u t)) 
-\to (arity g c2 u2 a2))) H21 Abbr H18) in (let H25 \def (eq_ind_r B b 
-(\lambda (b0: B).(\forall (c3: C).((wcpr0 (CHead c (Bind b0) u) c3) \to 
-(\forall (t5: T).((pr0 t t5) \to (arity g c3 t5 a2)))))) H4 Abbr H18) in (let 
-H26 \def (eq_ind_r B b (\lambda (b0: B).(arity g (CHead c (Bind b0) u) t a2)) 
-H3 Abbr H18) in (let H27 \def (eq_ind_r B b (\lambda (b0: B).(not (eq B b0 
-Abst))) H0 Abbr H18) in (arity_bind g Abbr H27 c2 u2 a1 (H2 c2 H5 u2 H22) w 
-a2 (arity_subst0 g (CHead c2 (Bind Abbr) u2) t4 a2 (H25 (CHead c2 (Bind Abbr) 
-u2) (wcpr0_comp c c2 H5 u u2 H22 (Bind Abbr)) t4 H20) c2 u2 O (getl_refl Abbr 
-c2 u2) w H12)))))))))))))) H15)) H14))))))))))))) (\lambda (b0: B).(\lambda 
-(H8: (not (eq B b0 Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: 
-(pr0 t3 t4)).(\lambda (H10: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 
-t4 a2)))).(\lambda (u0: T).(\lambda (H11: (eq T (THead (Bind b0) u0 (lift (S 
-O) O t3)) (THead (Bind b) u t))).(let H12 \def (f_equal T B (\lambda (e: 
-T).(match e in T return (\lambda (_: T).B) with [(TSort _) \Rightarrow b0 | 
-(TLRef _) \Rightarrow b0 | (THead k _ _) \Rightarrow (match k in K return 
-(\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow 
-b0])])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) 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 u0 | (TLRef _) \Rightarrow u0 | (THead _ t0 
-_) \Rightarrow t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) 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 ((let rec lref_map (f: ((nat 
-\to nat))) (d: nat) (t0: T) on t0: T \def (match t0 with [(TSort n) 
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with 
-[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u1 t5) 
-\Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d) t5))]) in 
-lref_map) (\lambda (x: nat).(plus x (S O))) O t3) | (TLRef _) \Rightarrow 
-((let rec lref_map (f: ((nat \to nat))) (d: nat) (t0: T) on t0: T \def (match 
-t0 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef 
-(match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | 
-(THead k u1 t5) \Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d) 
-t5))]) in lref_map) (\lambda (x: nat).(plus x (S O))) O t3) | (THead _ _ t0) 
-\Rightarrow t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u t) 
-H11) in (\lambda (_: (eq T u0 u)).(\lambda (H16: (eq B b0 b)).(let H17 \def 
-(eq_ind B b0 (\lambda (b1: B).(not (eq B b1 Abst))) H8 b H16) in (let H18 
-\def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead (Bind b) u t0)) \to 
+u H17) in (let H22 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H8 u H17) 
+in (let H23 \def (eq_ind_r B b (\lambda (b0: B).((eq T t (THead (Bind b0) u 
+t)) \to (arity g c2 t4 a2))) H19 Abbr H18) in (let H24 \def (eq_ind_r B b 
+(\lambda (b0: B).((eq T u (THead (Bind b0) u t)) \to (arity g c2 u2 a2))) H21 
+Abbr H18) in (let H25 \def (eq_ind_r B b (\lambda (b0: B).(\forall (c3: 
+C).((wcpr0 (CHead c (Bind b0) u) c3) \to (\forall (t5: T).((pr0 t t5) \to 
+(arity g c3 t5 a2)))))) H4 Abbr H18) in (let H26 \def (eq_ind_r B b (\lambda 
+(b0: B).(arity g (CHead c (Bind b0) u) t a2)) H3 Abbr H18) in (let H27 \def 
+(eq_ind_r B b (\lambda (b0: B).(not (eq B b0 Abst))) H0 Abbr H18) in 
+(arity_bind g Abbr H27 c2 u2 a1 (H2 c2 H5 u2 H22) w a2 (arity_subst0 g (CHead 
+c2 (Bind Abbr) u2) t4 a2 (H25 (CHead c2 (Bind Abbr) u2) (wcpr0_comp c c2 H5 u 
+u2 H22 (Bind Abbr)) t4 H20) c2 u2 O (getl_refl Abbr c2 u2) w 
+H12)))))))))))))) H15)) H14))))))))))))) (\lambda (b0: B).(\lambda (H8: (not 
+(eq B b0 Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 
+t4)).(\lambda (H10: (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 
+a2)))).(\lambda (u0: T).(\lambda (H11: (eq T (THead (Bind b0) u0 (lift (S O) 
+O t3)) (THead (Bind b) u t))).(let H12 \def (f_equal T B (\lambda (e: 
+T).(match e with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | 
+(THead k _ _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat _) 
+\Rightarrow b0])])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u 
+t) H11) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e with [(TSort 
+_) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t0 _) \Rightarrow 
+t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) u t) H11) in 
+((let H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
+\Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | (TLRef _) 
+\Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | (THead _ _ 
+t0) \Rightarrow t0])) (THead (Bind b0) u0 (lift (S O) O t3)) (THead (Bind b) 
+u t) H11) in (\lambda (_: (eq T u0 u)).(\lambda (H16: (eq B b0 b)).(let H17 
+\def (eq_ind B b0 (\lambda (b1: B).(not (eq B b1 Abst))) H8 b H16) in (let 
+H18 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead (Bind b) u t0)) \to 
 (arity g c2 t4 a2))) H10 (lift (S O) O t3) H14) in (let H19 \def (eq_ind_r T 
 t (\lambda (t0: T).(\forall (c3: C).((wcpr0 (CHead c (Bind b) u) c3) \to 
 (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 t5 a2)))))) H4 (lift (S O) O 
@@ -196,10 +181,9 @@ t3) H14) in (let H20 \def (eq_ind_r T t (\lambda (t0: T).(arity g (CHead c
 (\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: 
 (((eq T t3 (THead (Bind b) u t)) \to (arity g c2 t4 a2)))).(\lambda (u0: 
 T).(\lambda (H10: (eq T (THead (Flat Cast) u0 t3) (THead (Bind b) u t))).(let 
-H11 \def (eq_ind T (THead (Flat Cast) u0 t3) (\lambda (ee: T).(match ee in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda 
-(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
+H11 \def (eq_ind T (THead (Flat Cast) u0 t3) (\lambda (ee: T).(match ee with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
+\Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
 True])])) I (THead (Bind b) u t) H10) in (False_ind (arity g c2 t4 a2) 
 H11)))))))) y t2 H7))) H6)))))))))))))))) (\lambda (c: C).(\lambda (u: 
 T).(\lambda (a1: A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda (H1: 
@@ -223,34 +207,32 @@ T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1
 T).(\lambda (t4: T).(\lambda (H9: (pr0 t3 t4)).(\lambda (H10: (((eq T t3 
 (THead (Bind Abst) u t)) \to (arity g c2 t4 (AHead a1 a2))))).(\lambda (k: 
 K).(\lambda (H11: (eq T (THead k u1 t3) (THead (Bind Abst) 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 (Bind Abst) 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 (Bind Abst) 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 (Bind Abst) u t) H11) in (\lambda 
-(H15: (eq T u1 u)).(\lambda (H16: (eq K k (Bind Abst))).(eq_ind_r K (Bind 
-Abst) (\lambda (k0: K).(arity g c2 (THead k0 u2 t4) (AHead a1 a2))) (let H17 
-\def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Bind Abst) u t)) \to 
-(arity g c2 t4 (AHead a1 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 (Bind Abst) u t)) \to (arity g c2 u2 (AHead 
-a1 a2)))) H8 u H15) in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 
-u2)) H7 u H15) in (arity_head g c2 u2 a1 (H1 c2 H4 u2 H20) t4 a2 (H3 (CHead 
-c2 (Bind Abst) u2) (wcpr0_comp c c2 H4 u u2 H20 (Bind Abst)) t4 H18)))))) k 
-H16)))) H13)) H12)))))))))))) (\lambda (u0: T).(\lambda (v1: T).(\lambda (v2: 
-T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u t)) 
-\to (arity g c2 v2 (AHead a1 a2))))).(\lambda (t3: T).(\lambda (t4: 
-T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) 
-\to (arity g c2 t4 (AHead a1 a2))))).(\lambda (H11: (eq T (THead (Flat Appl) 
-v1 (THead (Bind Abst) u0 t3)) (THead (Bind Abst) u t))).(let H12 \def (eq_ind 
-T (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee 
-in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef 
-_) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return 
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
+\def (f_equal T K (\lambda (e: T).(match e with [(TSort _) \Rightarrow k | 
+(TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u1 t3) 
+(THead (Bind Abst) u t) H11) in ((let H13 \def (f_equal T T (\lambda (e: 
+T).(match e with [(TSort _) \Rightarrow u1 | (TLRef _) \Rightarrow u1 | 
+(THead _ t0 _) \Rightarrow t0])) (THead k u1 t3) (THead (Bind Abst) u t) H11) 
+in ((let H14 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
+\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t0) \Rightarrow t0])) 
+(THead k u1 t3) (THead (Bind Abst) u t) H11) in (\lambda (H15: (eq T u1 
+u)).(\lambda (H16: (eq K k (Bind Abst))).(eq_ind_r K (Bind Abst) (\lambda 
+(k0: K).(arity g c2 (THead k0 u2 t4) (AHead a1 a2))) (let H17 \def (eq_ind T 
+t3 (\lambda (t0: T).((eq T t0 (THead (Bind Abst) u t)) \to (arity g c2 t4 
+(AHead a1 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 (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 a2)))) H8 u H15) 
+in (let H20 \def (eq_ind T u1 (\lambda (t0: T).(pr0 t0 u2)) H7 u H15) in 
+(arity_head g c2 u2 a1 (H1 c2 H4 u2 H20) t4 a2 (H3 (CHead c2 (Bind Abst) u2) 
+(wcpr0_comp c c2 H4 u u2 H20 (Bind Abst)) t4 H18)))))) k H16)))) H13)) 
+H12)))))))))))) (\lambda (u0: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda 
+(_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u t)) \to (arity 
+g c2 v2 (AHead a1 a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
+t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 
+(AHead a1 a2))))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead (Bind 
+Abst) u0 t3)) (THead (Bind Abst) u t))).(let H12 \def (eq_ind T (THead (Flat 
+Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee with [(TSort 
+_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
+\Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
 True])])) I (THead (Bind Abst) u t) H11) in (False_ind (arity g c2 (THead 
 (Bind Abbr) v2 t4) (AHead a1 a2)) H12)))))))))))) (\lambda (b: B).(\lambda 
 (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 
@@ -261,214 +243,194 @@ u2)).(\lambda (_: (((eq T u1 (THead (Bind Abst) u t)) \to (arity g c2 u2
 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 
 (AHead a1 a2))))).(\lambda (H14: (eq T (THead (Flat Appl) v1 (THead (Bind b) 
 u1 t3)) (THead (Bind Abst) u t))).(let H15 \def (eq_ind T (THead (Flat Appl) 
-v1 (THead (Bind b) u1 t3)) (\lambda (ee: T).(match ee in T return (\lambda 
-(_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
-| (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
-[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind 
-Abst) u t) H14) in (False_ind (arity g c2 (THead (Bind b) u2 (THead (Flat 
-Appl) (lift (S O) O v2) t4)) (AHead a1 a2)) H15))))))))))))))))) (\lambda 
-(u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 
-(THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 a2))))).(\lambda (t3: 
-T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead 
-(Bind Abst) u t)) \to (arity g c2 t4 (AHead a1 a2))))).(\lambda (w: 
-T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T (THead (Bind Abbr) 
-u1 t3) (THead (Bind Abst) u t))).(let H13 \def (eq_ind T (THead (Bind Abbr) 
-u1 t3) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with 
-[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
-\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b) 
-\Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow 
-True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) 
-\Rightarrow False])])) I (THead (Bind Abst) u t) H12) in (False_ind (arity g 
-c2 (THead (Bind Abbr) u2 w) (AHead a1 a2)) H13))))))))))))) (\lambda (b: 
-B).(\lambda (H7: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: 
-T).(\lambda (_: (pr0 t3 t4)).(\lambda (H9: (((eq T t3 (THead (Bind Abst) u 
-t)) \to (arity g c2 t4 (AHead a1 a2))))).(\lambda (u0: T).(\lambda (H10: (eq 
-T (THead (Bind b) u0 (lift (S O) O t3)) (THead (Bind Abst) u t))).(let H11 
-\def (f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) 
-with [(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead k _ _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0) 
+v1 (THead (Bind b) u1 t3)) (\lambda (ee: T).(match ee with [(TSort _) 
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
+(match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I 
+(THead (Bind Abst) u t) H14) in (False_ind (arity g c2 (THead (Bind b) u2 
+(THead (Flat Appl) (lift (S O) O v2) t4)) (AHead a1 a2)) H15))))))))))))))))) 
+(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: 
+(((eq T u1 (THead (Bind Abst) u t)) \to (arity g c2 u2 (AHead a1 
+a2))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda 
+(_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 (AHead a1 
+a2))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T 
+(THead (Bind Abbr) u1 t3) (THead (Bind Abst) u t))).(let H13 \def (eq_ind T 
+(THead (Bind Abbr) u1 t3) (\lambda (ee: T).(match ee with [(TSort _) 
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
+(match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True | 
+Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow 
+False])])) I (THead (Bind Abst) u t) H12) in (False_ind (arity g c2 (THead 
+(Bind Abbr) u2 w) (AHead a1 a2)) H13))))))))))))) (\lambda (b: B).(\lambda 
+(H7: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
+t3 t4)).(\lambda (H9: (((eq T t3 (THead (Bind Abst) u t)) \to (arity g c2 t4 
+(AHead a1 a2))))).(\lambda (u0: T).(\lambda (H10: (eq T (THead (Bind b) u0 
+(lift (S O) O t3)) (THead (Bind Abst) u t))).(let H11 \def (f_equal T B 
+(\lambda (e: T).(match e with [(TSort _) \Rightarrow b | (TLRef _) 
+\Rightarrow b | (THead k _ _) \Rightarrow (match k with [(Bind b0) 
 \Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead (Bind b) u0 (lift (S O) O 
 t3)) (THead (Bind Abst) u t) H10) in ((let H12 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | 
-(TLRef _) \Rightarrow u0 | (THead _ t0 _) \Rightarrow t0])) (THead (Bind b) 
-u0 (lift (S O) O t3)) (THead (Bind Abst) u t) H10) in ((let H13 \def (f_equal 
-T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
-\Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t0: T) on t0: T 
-\def (match t0 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow 
-(TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) 
-| (THead k u1 t5) \Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d) 
-t5))]) in lref_map) (\lambda (x: nat).(plus x (S O))) O t3) | (TLRef _) 
-\Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t0: T) on t0: T 
-\def (match t0 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow 
-(TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) 
-| (THead k u1 t5) \Rightarrow (THead k (lref_map f d u1) (lref_map f (s k d) 
-t5))]) in lref_map) (\lambda (x: nat).(plus x (S O))) O t3) | (THead _ _ t0) 
-\Rightarrow t0])) (THead (Bind b) u0 (lift (S O) O t3)) (THead (Bind Abst) u 
-t) H10) in (\lambda (_: (eq T u0 u)).(\lambda (H15: (eq B b Abst)).(let H16 
-\def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H7 Abst H15) in (let 
-H17 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead (Bind Abst) u t0)) 
-\to (arity g c2 t4 (AHead a1 a2)))) H9 (lift (S O) O t3) H13) in (let H18 
-\def (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0 (CHead c (Bind 
-Abst) u) c3) \to (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 t5 a2)))))) H3 
-(lift (S O) O t3) H13) in (let H19 \def (eq_ind_r T t (\lambda (t0: T).(arity 
-g (CHead c (Bind Abst) u) t0 a2)) H2 (lift (S O) O t3) H13) in (let H20 \def 
-(match (H16 (refl_equal B Abst)) in False return (\lambda (_: False).(arity g 
-c2 t4 (AHead a1 a2))) with []) in H20)))))))) H12)) H11)))))))))) (\lambda 
-(t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 
-(THead (Bind Abst) u t)) \to (arity g c2 t4 (AHead a1 a2))))).(\lambda (u0: 
-T).(\lambda (H9: (eq T (THead (Flat Cast) u0 t3) (THead (Bind Abst) u 
-t))).(let H10 \def (eq_ind T (THead (Flat Cast) u0 t3) (\lambda (ee: 
-T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K 
-return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
-\Rightarrow True])])) I (THead (Bind Abst) u t) H9) in (False_ind (arity g c2 
-t4 (AHead a1 a2)) H10)))))))) y t2 H6))) H5)))))))))))))) (\lambda (c: 
-C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda 
-(H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 u t2) \to 
-(arity g c2 t2 a1))))))).(\lambda (t: T).(\lambda (a2: A).(\lambda (H2: 
-(arity g c t (AHead a1 a2))).(\lambda (H3: ((\forall (c2: C).((wcpr0 c c2) 
-\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)) (\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 (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: 
-B).(\lambda (H7: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: 
-T).(\lambda (H8: (pr0 v1 v2)).(\lambda (H9: (((eq T v1 (THead (Flat Appl) u 
-t)) \to (arity g c2 v2 a2)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda 
-(H10: (pr0 u1 u2)).(\lambda (H11: (((eq T u1 (THead (Flat Appl) u t)) \to 
-(arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H12: (pr0 
-t3 t4)).(\lambda (H13: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g c2 t4 
-a2)))).(\lambda (H14: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) 
-(THead (Flat Appl) u t))).(let H15 \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 b) u1 t3)) (THead (Flat Appl) u t) H14) in ((let H16 \def 
-(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
-[(TSort _) \Rightarrow (THead (Bind b) u1 t3) | (TLRef _) \Rightarrow (THead 
-(Bind b) u1 t3) | (THead _ _ t0) \Rightarrow t0])) (THead (Flat Appl) v1 
-(THead (Bind b) u1 t3)) (THead (Flat Appl) u t) H14) in (\lambda (H17: (eq T 
-v1 u)).(let H18 \def (eq_ind T v1 (\lambda (t0: T).((eq T t0 (THead (Flat 
-Appl) u t)) \to (arity g c2 v2 a2))) H9 u H17) in (let H19 \def (eq_ind T v1 
-(\lambda (t0: T).(pr0 t0 v2)) H8 u H17) in (let H20 \def (eq_ind_r T t 
-(\lambda (t0: T).((eq T t3 (THead (Flat Appl) u t0)) \to (arity g c2 t4 a2))) 
-H13 (THead (Bind b) u1 t3) H16) in (let H21 \def (eq_ind_r T t (\lambda (t0: 
-T).((eq T u1 (THead (Flat Appl) u t0)) \to (arity g c2 u2 a2))) H11 (THead 
-(Bind b) u1 t3) H16) in (let H22 \def (eq_ind_r T t (\lambda (t0: T).((eq T u 
-(THead (Flat Appl) u t0)) \to (arity g c2 v2 a2))) H18 (THead (Bind b) u1 t3) 
-H16) in (let H23 \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 b) u1 t3) H16) in (let H24 \def (eq_ind_r T t 
-(\lambda (t0: T).(arity g c t0 (AHead a1 a2))) H2 (THead (Bind b) u1 t3) H16) 
-in (let H25 \def (H1 c2 H4 v2 H19) in (let H26 \def (H23 c2 H4 (THead (Bind 
-b) u2 t4) (pr0_comp u1 u2 H10 t3 t4 H12 (Bind b))) in (let H27 \def 
-(arity_gen_bind b H7 g c2 u2 t4 (AHead a1 a2) H26) in (ex2_ind A (\lambda 
-(a3: A).(arity g c2 u2 a3)) (\lambda (_: A).(arity g (CHead c2 (Bind b) u2) 
-t4 (AHead a1 a2))) (arity g c2 (THead (Bind b) u2 (THead (Flat Appl) (lift (S 
-O) O v2) t4)) a2) (\lambda (x: A).(\lambda (H28: (arity g c2 u2 x)).(\lambda 
-(H29: (arity g (CHead c2 (Bind b) u2) t4 (AHead a1 a2))).(arity_bind g b H7 
-c2 u2 x H28 (THead (Flat Appl) (lift (S O) O v2) t4) a2 (arity_appl g (CHead 
-c2 (Bind b) u2) (lift (S O) O v2) a1 (arity_lift g c2 v2 a1 H25 (CHead c2 
-(Bind b) u2) (S O) O (drop_drop (Bind b) O c2 c2 (drop_refl c2) u2)) t4 a2 
-H29))))) H27))))))))))))) H15))))))))))))))))) (\lambda (u1: T).(\lambda (u2: 
-T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead (Flat Appl) u t)) 
-\to (arity g c2 u2 a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
-t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g c2 t4 
-a2)))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T 
-(THead (Bind Abbr) u1 t3) (THead (Flat Appl) u t))).(let H13 \def (eq_ind T 
-(THead (Bind Abbr) u1 t3) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
-(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
-[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat 
-Appl) u t) H12) in (False_ind (arity g c2 (THead (Bind Abbr) u2 w) a2) 
+T).(match e with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | 
+(THead _ t0 _) \Rightarrow t0])) (THead (Bind b) u0 (lift (S O) O t3)) (THead 
+(Bind Abst) u t) H10) in ((let H13 \def (f_equal T T (\lambda (e: T).(match e 
+with [(TSort _) \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) 
+| (TLRef _) \Rightarrow (lref_map (\lambda (x: nat).(plus x (S O))) O t3) | 
+(THead _ _ t0) \Rightarrow t0])) (THead (Bind b) u0 (lift (S O) O t3)) (THead 
+(Bind Abst) u t) H10) in (\lambda (_: (eq T u0 u)).(\lambda (H15: (eq B b 
+Abst)).(let H16 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H7 
+Abst H15) in (let H17 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead 
+(Bind Abst) u t0)) \to (arity g c2 t4 (AHead a1 a2)))) H9 (lift (S O) O t3) 
+H13) in (let H18 \def (eq_ind_r T t (\lambda (t0: T).(\forall (c3: C).((wcpr0 
+(CHead c (Bind Abst) u) c3) \to (\forall (t5: T).((pr0 t0 t5) \to (arity g c3 
+t5 a2)))))) H3 (lift (S O) O t3) H13) in (let H19 \def (eq_ind_r T t (\lambda 
+(t0: T).(arity g (CHead c (Bind Abst) u) t0 a2)) H2 (lift (S O) O t3) H13) in 
+(let H20 \def (match (H16 (refl_equal B Abst)) in False with []) in 
+H20)))))))) H12)) H11)))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda 
+(_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Bind Abst) u t)) \to (arity 
+g c2 t4 (AHead a1 a2))))).(\lambda (u0: T).(\lambda (H9: (eq T (THead (Flat 
+Cast) u0 t3) (THead (Bind Abst) u t))).(let H10 \def (eq_ind T (THead (Flat 
+Cast) u0 t3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | 
+(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind 
+_) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) u 
+t) H9) in (False_ind (arity g c2 t4 (AHead a1 a2)) H10)))))))) y t2 H6))) 
+H5)))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda 
+(_: (arity g c u a1)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to 
+(\forall (t2: T).((pr0 u t2) \to (arity g c2 t2 a1))))))).(\lambda (t: 
+T).(\lambda (a2: A).(\lambda (H2: (arity g c t (AHead a1 a2))).(\lambda (H3: 
+((\forall (c2: C).((wcpr0 c c2) \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)) 
+(\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 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 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 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 
+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 
+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 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 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: B).(\lambda (H7: (not (eq B b 
+Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H8: (pr0 v1 v2)).(\lambda 
+(H9: (((eq T v1 (THead (Flat Appl) u t)) \to (arity g c2 v2 a2)))).(\lambda 
+(u1: T).(\lambda (u2: T).(\lambda (H10: (pr0 u1 u2)).(\lambda (H11: (((eq T 
+u1 (THead (Flat Appl) u t)) \to (arity g c2 u2 a2)))).(\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (H12: (pr0 t3 t4)).(\lambda (H13: (((eq T t3 
+(THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (H14: (eq T 
+(THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Appl) u t))).(let 
+H15 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow v1 
+| (TLRef _) \Rightarrow v1 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat 
+Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Appl) u t) H14) in ((let H16 
+\def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (THead 
+(Bind b) u1 t3) | (TLRef _) \Rightarrow (THead (Bind b) u1 t3) | (THead _ _ 
+t0) \Rightarrow t0])) (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (THead 
+(Flat Appl) u t) H14) in (\lambda (H17: (eq T v1 u)).(let H18 \def (eq_ind T 
+v1 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) u t)) \to (arity g c2 v2 
+a2))) H9 u H17) in (let H19 \def (eq_ind T v1 (\lambda (t0: T).(pr0 t0 v2)) 
+H8 u H17) in (let H20 \def (eq_ind_r T t (\lambda (t0: T).((eq T t3 (THead 
+(Flat Appl) u t0)) \to (arity g c2 t4 a2))) H13 (THead (Bind b) u1 t3) H16) 
+in (let H21 \def (eq_ind_r T t (\lambda (t0: T).((eq T u1 (THead (Flat Appl) 
+u t0)) \to (arity g c2 u2 a2))) H11 (THead (Bind b) u1 t3) H16) in (let H22 
+\def (eq_ind_r T t (\lambda (t0: T).((eq T u (THead (Flat Appl) u t0)) \to 
+(arity g c2 v2 a2))) H18 (THead (Bind b) u1 t3) H16) in (let H23 \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 
+b) u1 t3) H16) in (let H24 \def (eq_ind_r T t (\lambda (t0: T).(arity g c t0 
+(AHead a1 a2))) H2 (THead (Bind b) u1 t3) H16) in (let H25 \def (H1 c2 H4 v2 
+H19) in (let H26 \def (H23 c2 H4 (THead (Bind b) u2 t4) (pr0_comp u1 u2 H10 
+t3 t4 H12 (Bind b))) in (let H27 \def (arity_gen_bind b H7 g c2 u2 t4 (AHead 
+a1 a2) H26) in (ex2_ind A (\lambda (a3: A).(arity g c2 u2 a3)) (\lambda (_: 
+A).(arity g (CHead c2 (Bind b) u2) t4 (AHead a1 a2))) (arity g c2 (THead 
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) a2) (\lambda (x: 
+A).(\lambda (H28: (arity g c2 u2 x)).(\lambda (H29: (arity g (CHead c2 (Bind 
+b) u2) t4 (AHead a1 a2))).(arity_bind g b H7 c2 u2 x H28 (THead (Flat Appl) 
+(lift (S O) O v2) t4) a2 (arity_appl g (CHead c2 (Bind b) u2) (lift (S O) O 
+v2) a1 (arity_lift g c2 v2 a1 H25 (CHead c2 (Bind b) u2) (S O) O (drop_drop 
+(Bind b) O c2 c2 (drop_refl c2) u2)) t4 a2 H29))))) H27))))))))))))) 
+H15))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 
+u2)).(\lambda (_: (((eq T u1 (THead (Flat Appl) u t)) \to (arity g c2 u2 
+a2)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda 
+(_: (((eq T t3 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda 
+(w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T (THead (Bind 
+Abbr) u1 t3) (THead (Flat Appl) u t))).(let H13 \def (eq_ind T (THead (Bind 
+Abbr) u1 t3) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | 
+(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind 
+_) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u 
+t) H12) in (False_ind (arity g c2 (THead (Bind Abbr) u2 w) a2) 
 H13))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda 
 (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 
 (THead (Flat Appl) u t)) \to (arity g c2 t4 a2)))).(\lambda (u0: T).(\lambda 
 (H10: (eq T (THead (Bind b) u0 (lift (S O) O t3)) (THead (Flat Appl) u 
 t))).(let H11 \def (eq_ind T (THead (Bind b) u0 (lift (S O) O t3)) (\lambda 
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
-(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | 
+(ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow 
+False | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | 
 (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u t) H10) in (False_ind 
 (arity g c2 t4 a2) H11)))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda 
 (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Appl) u t)) \to (arity 
 g c2 t4 a2)))).(\lambda (u0: T).(\lambda (H9: (eq T (THead (Flat Cast) u0 t3) 
 (THead (Flat Appl) u t))).(let H10 \def (eq_ind T (THead (Flat Cast) u0 t3) 
-(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
-(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | 
-(Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl 
-\Rightarrow False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t) 
-H9) in (False_ind (arity g c2 t4 a2) H10)))))))) y t2 H6))) H5)))))))))))))) 
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) 
+\Rightarrow False | (Flat f) \Rightarrow (match f with [Appl \Rightarrow 
+False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t) H9) in 
+(False_ind (arity g c2 t4 a2) H10)))))))) y t2 H6))) H5)))))))))))))) 
 (\lambda (c: C).(\lambda (u: T).(\lambda (a0: A).(\lambda (_: (arity g c u 
 (asucc g a0))).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall 
 (t2: T).((pr0 u t2) \to (arity g c2 t2 (asucc g a0)))))))).(\lambda (t: 
@@ -488,18 +450,17 @@ T).(\lambda (u2: T).(\lambda (H7: (pr0 u1 u2)).(\lambda (H8: (((eq T u1
 (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 
+(e: T).(match e 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 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 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)) 
@@ -510,71 +471,63 @@ T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead
 T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) 
 \to (arity g c2 t4 a0)))).(\lambda (H11: (eq T (THead (Flat Appl) v1 (THead 
 (Bind Abst) u0 t3)) (THead (Flat Cast) u t))).(let H12 \def (eq_ind T (THead 
-(Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda 
-(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f 
-in F return (\lambda (_: F).Prop) with [Appl \Rightarrow True | Cast 
-\Rightarrow False])])])) I (THead (Flat Cast) u t) H11) in (False_ind (arity 
-g c2 (THead (Bind Abbr) v2 t4) a0) H12)))))))))))) (\lambda (b: B).(\lambda 
-(_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 
-v1 v2)).(\lambda (_: (((eq T v1 (THead (Flat Cast) u t)) \to (arity g c2 v2 
-a0)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda 
-(_: (((eq T u1 (THead (Flat Cast) u t)) \to (arity g c2 u2 a0)))).(\lambda 
-(t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 
-(THead (Flat Cast) u t)) \to (arity g c2 t4 a0)))).(\lambda (H14: (eq T 
-(THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (THead (Flat Cast) u t))).(let 
-H15 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1 t3)) (\lambda 
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
+(Flat Appl) v1 (THead (Bind Abst) u0 t3)) (\lambda (ee: T).(match ee with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) 
+\Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow 
+(match f with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead 
+(Flat Cast) u t) H11) in (False_ind (arity g c2 (THead (Bind Abbr) v2 t4) a0) 
+H12)))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda 
+(v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 
+(THead (Flat Cast) u t)) \to (arity g c2 v2 a0)))).(\lambda (u1: T).(\lambda 
+(u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead (Flat Cast) 
+u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda 
+(_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) \to (arity 
+g c2 t4 a0)))).(\lambda (H14: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1 
+t3)) (THead (Flat Cast) u t))).(let H15 \def (eq_ind T (THead (Flat Appl) v1 
+(THead (Bind b) u1 t3)) (\lambda (ee: T).(match ee with [(TSort _) 
 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
-(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | 
-(Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl 
-\Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat Cast) u t) 
-H14) in (False_ind (arity g c2 (THead (Bind b) u2 (THead (Flat Appl) (lift (S 
-O) O v2) t4)) a0) H15))))))))))))))))) (\lambda (u1: T).(\lambda (u2: 
-T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead (Flat Cast) u t)) 
-\to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
+(match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f 
+with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat 
+Cast) u t) H14) in (False_ind (arity g c2 (THead (Bind b) u2 (THead (Flat 
+Appl) (lift (S O) O v2) t4)) a0) H15))))))))))))))))) (\lambda (u1: 
+T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (THead 
+(Flat Cast) u t)) \to (arity g c2 u2 a0)))).(\lambda (t3: T).(\lambda (t4: 
+T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) 
+\to (arity g c2 t4 a0)))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4 
+w)).(\lambda (H12: (eq T (THead (Bind Abbr) u1 t3) (THead (Flat Cast) u 
+t))).(let H13 \def (eq_ind T (THead (Bind Abbr) u1 t3) (\lambda (ee: 
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
+| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat 
+_) \Rightarrow False])])) I (THead (Flat Cast) u t) H12) in (False_ind (arity 
+g c2 (THead (Bind Abbr) u2 w) a0) H13))))))))))))) (\lambda (b: B).(\lambda 
+(_: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 
 t3 t4)).(\lambda (_: (((eq T t3 (THead (Flat Cast) u t)) \to (arity g c2 t4 
-a0)))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t4 w)).(\lambda (H12: (eq T 
-(THead (Bind Abbr) u1 t3) (THead (Flat Cast) u t))).(let H13 \def (eq_ind T 
-(THead (Bind Abbr) u1 t3) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
-(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
+a0)))).(\lambda (u0: T).(\lambda (H10: (eq T (THead (Bind b) u0 (lift (S O) O 
+t3)) (THead (Flat Cast) u t))).(let H11 \def (eq_ind T (THead (Bind b) u0 
+(lift (S O) O t3)) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow 
+False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with 
 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat 
-Cast) u t) H12) in (False_ind (arity g c2 (THead (Bind Abbr) u2 w) a0) 
-H13))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda 
-(t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (_: (((eq T t3 
+Cast) u t) H10) in (False_ind (arity g c2 t4 a0) H11)))))))))) (\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (H7: (pr0 t3 t4)).(\lambda (H8: (((eq T t3 
 (THead (Flat Cast) u t)) \to (arity g c2 t4 a0)))).(\lambda (u0: T).(\lambda 
-(H10: (eq T (THead (Bind b) u0 (lift (S O) O t3)) (THead (Flat Cast) u 
-t))).(let H11 \def (eq_ind T (THead (Bind b) u0 (lift (S O) O t3)) (\lambda 
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
-(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | 
-(Flat _) \Rightarrow False])])) I (THead (Flat Cast) u t) H10) in (False_ind 
-(arity g c2 t4 a0) H11)))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda 
-(H7: (pr0 t3 t4)).(\lambda (H8: (((eq T t3 (THead (Flat Cast) u t)) \to 
-(arity g c2 t4 a0)))).(\lambda (u0: T).(\lambda (H9: (eq T (THead (Flat Cast) 
-u0 t3) (THead (Flat Cast) u t))).(let H10 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | 
-(TLRef _) \Rightarrow u0 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat 
-Cast) u0 t3) (THead (Flat Cast) u t) H9) in ((let H11 \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 (Flat Cast) u0 t3) (THead (Flat Cast) u t) H9) in (\lambda (_: (eq T 
-u0 u)).(let H13 \def (eq_ind T t3 (\lambda (t0: T).((eq T t0 (THead (Flat 
-Cast) u t)) \to (arity g c2 t4 a0))) H8 t H11) in (let H14 \def (eq_ind T t3 
-(\lambda (t0: T).(pr0 t0 t4)) H7 t H11) in (H3 c2 H4 t4 H14))))) H10)))))))) 
-y t2 H6))) H5))))))))))))) (\lambda (c: C).(\lambda (t: T).(\lambda (a1: 
-A).(\lambda (_: (arity g c t a1)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c 
-c2) \to (\forall (t2: T).((pr0 t t2) \to (arity g c2 t2 a1))))))).(\lambda 
-(a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: C).(\lambda (H3: (wcpr0 c 
-c2)).(\lambda (t2: T).(\lambda (H4: (pr0 t t2)).(arity_repl g c2 t2 a1 (H1 c2 
-H3 t2 H4) a2 H2)))))))))))) c1 t1 a H))))).
-(* COMMENTS
-Initial nodes: 10246
-END *)
+(H9: (eq T (THead (Flat Cast) u0 t3) (THead (Flat Cast) u t))).(let H10 \def 
+(f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 | (TLRef 
+_) \Rightarrow u0 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat Cast) u0 
+t3) (THead (Flat Cast) u t) H9) in ((let H11 \def (f_equal T T (\lambda (e: 
+T).(match e with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | 
+(THead _ _ t0) \Rightarrow t0])) (THead (Flat Cast) u0 t3) (THead (Flat Cast) 
+u t) H9) in (\lambda (_: (eq T u0 u)).(let H13 \def (eq_ind T t3 (\lambda 
+(t0: T).((eq T t0 (THead (Flat Cast) u t)) \to (arity g c2 t4 a0))) H8 t H11) 
+in (let H14 \def (eq_ind T t3 (\lambda (t0: T).(pr0 t0 t4)) H7 t H11) in (H3 
+c2 H4 t4 H14))))) H10)))))))) y t2 H6))) H5))))))))))))) (\lambda (c: 
+C).(\lambda (t: T).(\lambda (a1: A).(\lambda (_: (arity g c t a1)).(\lambda 
+(H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 t t2) \to 
+(arity g c2 t2 a1))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 
+a2)).(\lambda (c2: C).(\lambda (H3: (wcpr0 c c2)).(\lambda (t2: T).(\lambda 
+(H4: (pr0 t t2)).(arity_repl g c2 t2 a1 (H1 c2 H3 t2 H4) a2 H2)))))))))))) c1 
+t1 a H))))).
 
-theorem arity_sred_wcpr0_pr1:
+lemma arity_sred_wcpr0_pr1:
  \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall 
 (c1: C).(\forall (a: A).((arity g c1 t1 a) \to (\forall (c2: C).((wcpr0 c1 
 c2) \to (arity g c2 t2 a)))))))))
@@ -592,11 +545,8 @@ a))))))))).(\lambda (g: G).(\lambda (c1: C).(\lambda (a: A).(\lambda (H3:
 (arity g c1 t4 a)).(\lambda (c2: C).(\lambda (H4: (wcpr0 c1 c2)).(H2 g c2 a 
 (arity_sred_wcpr0_pr0 g c1 t4 a H3 c2 H4 t3 H0) c2 (wcpr0_refl 
 c2)))))))))))))) t1 t2 H))).
-(* COMMENTS
-Initial nodes: 213
-END *)
 
-theorem arity_sred_pr2:
+lemma arity_sred_pr2:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
 (g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
 \def
@@ -612,11 +562,8 @@ t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (g:
 G).(\lambda (a: A).(\lambda (H3: (arity g c0 t3 a)).(arity_subst0 g c0 t4 a 
 (arity_sred_wcpr0_pr0 g c0 t3 a H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t 
 H2)))))))))))))) c t1 t2 H)))).
-(* COMMENTS
-Initial nodes: 205
-END *)
 
-theorem arity_sred_pr3:
+lemma arity_sred_pr3:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall 
 (g: G).(\forall (a: A).((arity g c t1 a) \to (arity g c t2 a)))))))
 \def
@@ -629,7 +576,4 @@ T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda
 t3 a) \to (arity g c t5 a)))))).(\lambda (g: G).(\lambda (a: A).(\lambda (H3: 
 (arity g c t4 a)).(H2 g a (arity_sred_pr2 c t4 t3 H0 g a H3))))))))))) t1 t2 
 H)))).
-(* COMMENTS
-Initial nodes: 151
-END *)