-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)