-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