-b0])])) (THead (Bind b0) u0 (lift (S O) O t6)) (THead (Bind b) u t2) H10) in
-(eq_ind B b (\lambda (b1: B).((eq T u0 u) \to ((eq T (lift (S O) O t6) t2)
-\to ((eq T t7 t5) \to ((not (eq B b1 Abst)) \to ((pr0 t6 t7) \to (ty3 g c2 t5
-(THead (Bind b) u t3)))))))) (\lambda (H15: (eq T u0 u)).(eq_ind T u (\lambda
-(_: T).((eq T (lift (S O) O t6) t2) \to ((eq T t7 t5) \to ((not (eq B b
-Abst)) \to ((pr0 t6 t7) \to (ty3 g c2 t5 (THead (Bind b) u t3))))))) (\lambda
-(H16: (eq T (lift (S O) O t6) t2)).(eq_ind T (lift (S O) O t6) (\lambda (_:
-T).((eq T t7 t5) \to ((not (eq B b Abst)) \to ((pr0 t6 t7) \to (ty3 g c2 t5
-(THead (Bind b) u t3)))))) (\lambda (H17: (eq T t7 t5)).(eq_ind T t5 (\lambda
-(t8: T).((not (eq B b Abst)) \to ((pr0 t6 t8) \to (ty3 g c2 t5 (THead (Bind
-b) u t3))))) (\lambda (H18: (not (eq B b Abst))).(\lambda (H19: (pr0 t6
-t5)).(let H20 \def (eq_ind_r T t2 (\lambda (t8: T).(\forall (c3: C).((wcpr0
-(CHead c (Bind b) u) c3) \to (\forall (t9: T).((pr0 t8 t9) \to (ty3 g c3 t9
-t3)))))) H3 (lift (S O) O t6) H16) in (let H21 \def (eq_ind_r T t2 (\lambda
-(t8: T).(ty3 g (CHead c (Bind b) u) t8 t3)) H2 (lift (S O) O t6) H16) in
-(ex_ind T (\lambda (t8: T).(ty3 g (CHead c2 (Bind b) u) t4 t8)) (ty3 g c2 t5
-(THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H22: (ty3 g (CHead c2 (Bind
-b) u) t4 x)).(B_ind (\lambda (b1: B).((not (eq B b1 Abst)) \to ((ty3 g (CHead
-c2 (Bind b1) u) t3 t4) \to ((ty3 g (CHead c2 (Bind b1) u) t4 x) \to ((ty3 g
-(CHead c2 (Bind b1) u) (lift (S O) O t5) t3) \to (ty3 g c2 t5 (THead (Bind
-b1) u t3))))))) (\lambda (H23: (not (eq B Abbr Abst))).(\lambda (H24: (ty3 g
-(CHead c2 (Bind Abbr) u) t3 t4)).(\lambda (H25: (ty3 g (CHead c2 (Bind Abbr)
-u) t4 x)).(\lambda (H26: (ty3 g (CHead c2 (Bind Abbr) u) (lift (S O) O t5)
-t3)).(let H27 \def (ty3_gen_cabbr g (CHead c2 (Bind Abbr) u) (lift (S O) O
-t5) t3 H26 c2 u O (getl_refl Abbr c2 u) (CHead c2 (Bind Abbr) u)
-(csubst1_refl O u (CHead c2 (Bind Abbr) u)) c2 (drop_drop (Bind Abbr) O c2 c2
-(drop_refl c2) u)) in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_: T).(subst1
-O u (lift (S O) O t5) (lift (S O) O y1)))) (\lambda (_: T).(\lambda (y2:
-T).(subst1 O u t3 (lift (S O) O y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3
-g c2 y1 y2))) (ty3 g c2 t5 (THead (Bind Abbr) u t3)) (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (H28: (subst1 O u (lift (S O) O t5) (lift (S O)
-O x0))).(\lambda (H29: (subst1 O u t3 (lift (S O) O x1))).(\lambda (H30: (ty3
-g c2 x0 x1)).(let H31 \def (eq_ind T x0 (\lambda (t8: T).(ty3 g c2 t8 x1))
-H30 t5 (lift_inj x0 t5 (S O) O (subst1_gen_lift_eq t5 u (lift (S O) O x0) (S
-O) O O (le_n O) (eq_ind_r nat (plus (S O) O) (\lambda (n: nat).(lt O n))
-(le_n (plus (S O) O)) (plus O (S O)) (plus_comm O (S O))) H28))) in (ty3_conv
-g c2 (THead (Bind Abbr) u t3) (THead (Bind Abbr) u t4) (ty3_bind g c2 u t0
-(H1 c2 H6 u (pr0_refl u)) Abbr t3 t4 H24 x H25) t5 x1 H31 (pc3_pr3_x c2 x1
-(THead (Bind Abbr) u t3) (pr3_t (THead (Bind Abbr) u (lift (S O) O x1))
-(THead (Bind Abbr) u t3) c2 (pr3_pr2 c2 (THead (Bind Abbr) u t3) (THead (Bind
-Abbr) u (lift (S O) O x1)) (pr2_free c2 (THead (Bind Abbr) u t3) (THead (Bind
-Abbr) u (lift (S O) O x1)) (pr0_delta1 u u (pr0_refl u) t3 t3 (pr0_refl t3)
-(lift (S O) O x1) H29))) x1 (pr3_pr2 c2 (THead (Bind Abbr) u (lift (S O) O
-x1)) x1 (pr2_free c2 (THead (Bind Abbr) u (lift (S O) O x1)) x1 (pr0_zeta
-Abbr H23 x1 x1 (pr0_refl x1) u)))))))))))) H27)))))) (\lambda (H23: (not (eq
-B Abst Abst))).(\lambda (_: (ty3 g (CHead c2 (Bind Abst) u) t3 t4)).(\lambda
-(_: (ty3 g (CHead c2 (Bind Abst) u) t4 x)).(\lambda (_: (ty3 g (CHead c2
-(Bind Abst) u) (lift (S O) O t5) t3)).(let H27 \def (match (H23 (refl_equal B
-Abst)) in False return (\lambda (_: False).(ty3 g c2 t5 (THead (Bind Abst) u
-t3))) with []) in H27))))) (\lambda (H23: (not (eq B Void Abst))).(\lambda
-(H24: (ty3 g (CHead c2 (Bind Void) u) t3 t4)).(\lambda (H25: (ty3 g (CHead c2
-(Bind Void) u) t4 x)).(\lambda (H26: (ty3 g (CHead c2 (Bind Void) u) (lift (S
-O) O t5) t3)).(let H27 \def (ty3_gen_cvoid g (CHead c2 (Bind Void) u) (lift
-(S O) O t5) t3 H26 c2 u O (getl_refl Void c2 u) c2 (drop_drop (Bind Void) O
-c2 c2 (drop_refl c2) u)) in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_:
-T).(eq T (lift (S O) O t5) (lift (S O) O y1)))) (\lambda (_: T).(\lambda (y2:
-T).(eq T t3 (lift (S O) O y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g c2
-y1 y2))) (ty3 g c2 t5 (THead (Bind Void) u t3)) (\lambda (x0: T).(\lambda
-(x1: T).(\lambda (H28: (eq T (lift (S O) O t5) (lift (S O) O x0))).(\lambda
-(H29: (eq T t3 (lift (S O) O x1))).(\lambda (H30: (ty3 g c2 x0 x1)).(let H31
-\def (eq_ind T t3 (\lambda (t8: T).(ty3 g (CHead c2 (Bind Void) u) t8 t4))
-H24 (lift (S O) O x1) H29) in (eq_ind_r T (lift (S O) O x1) (\lambda (t8:
-T).(ty3 g c2 t5 (THead (Bind Void) u t8))) (let H32 \def (eq_ind_r T x0
-(\lambda (t8: T).(ty3 g c2 t8 x1)) H30 t5 (lift_inj t5 x0 (S O) O H28)) in
-(ty3_conv g c2 (THead (Bind Void) u (lift (S O) O x1)) (THead (Bind Void) u
-t4) (ty3_bind g c2 u t0 (H1 c2 H6 u (pr0_refl u)) Void (lift (S O) O x1) t4
-H31 x H25) t5 x1 H32 (pc3_pr2_x c2 x1 (THead (Bind Void) u (lift (S O) O x1))
-(pr2_free c2 (THead (Bind Void) u (lift (S O) O x1)) x1 (pr0_zeta Void H23 x1
-x1 (pr0_refl x1) u))))) t3 H29))))))) H27)))))) b H18 (H5 (CHead c2 (Bind b)
-u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) t3 (pr0_refl t3)) H22 (H20
-(CHead c2 (Bind b) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind b)) (lift (S
-O) O t5) (pr0_lift t6 t5 H19 (S O) O))))) (ty3_correct g (CHead c2 (Bind b)
-u) t3 t4 (H5 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H6 u u (pr0_refl u) (Bind
-b)) t3 (pr0_refl t3)))))))) t7 (sym_eq T t7 t5 H17))) t2 H16)) u0 (sym_eq T
-u0 u H15))) b0 (sym_eq B b0 b H14))) H13)) H12)) H11 H8 H9))) | (pr0_epsilon
-t6 t7 H8 u0) \Rightarrow (\lambda (H9: (eq T (THead (Flat Cast) u0 t6) (THead
-(Bind b) u t2))).(\lambda (H10: (eq T t7 t5)).((let H11 \def (eq_ind T (THead
-(Flat Cast) u0 t6) (\lambda (e: T).(match e 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 t2)
-H9) in (False_ind ((eq T t7 t5) \to ((pr0 t6 t7) \to (ty3 g c2 t5 (THead
-(Bind b) u t3)))) H11)) H10 H8)))]) in (H8 (refl_equal T (THead (Bind b) u
-t2)) (refl_equal T t5)))))))))))))))))))) (\lambda (c: C).(\lambda (w:
-T).(\lambda (u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1: ((\forall (c2:
-C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 w t2) \to (ty3 g c2 t2
-u))))))).(\lambda (v: T).(\lambda (t0: T).(\lambda (H2: (ty3 g c v (THead
-(Bind Abst) u t0))).(\lambda (H3: ((\forall (c2: C).((wcpr0 c c2) \to
-(\forall (t2: T).((pr0 v t2) \to (ty3 g c2 t2 (THead (Bind Abst) u
-t0)))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c c2)).(\lambda (t2:
-T).(\lambda (H5: (pr0 (THead (Flat Appl) w v) t2)).(let H6 \def (match H5 in
-pr0 return (\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).((eq T
-t3 (THead (Flat Appl) w v)) \to ((eq T t4 t2) \to (ty3 g c2 t2 (THead (Flat
-Appl) w (THead (Bind Abst) u t0)))))))) with [(pr0_refl t3) \Rightarrow
-(\lambda (H6: (eq T t3 (THead (Flat Appl) w v))).(\lambda (H7: (eq T t3
-t2)).(eq_ind T (THead (Flat Appl) w v) (\lambda (t4: T).((eq T t4 t2) \to
-(ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))) (\lambda (H8:
-(eq T (THead (Flat Appl) w v) t2)).(eq_ind T (THead (Flat Appl) w v) (\lambda
-(t4: T).(ty3 g c2 t4 (THead (Flat Appl) w (THead (Bind Abst) u t0))))
-(ty3_appl g c2 w u (H1 c2 H4 w (pr0_refl w)) v t0 (H3 c2 H4 v (pr0_refl v)))
-t2 H8)) t3 (sym_eq T t3 (THead (Flat Appl) w v) H6) H7))) | (pr0_comp u1 u2
-H6 t3 t4 H7 k) \Rightarrow (\lambda (H8: (eq T (THead k u1 t3) (THead (Flat
-Appl) w v))).(\lambda (H9: (eq T (THead k u2 t4) t2)).((let H10 \def (f_equal
-T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
-\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t5) \Rightarrow t5]))
-(THead k u1 t3) (THead (Flat Appl) w v) H8) in ((let H11 \def (f_equal T T
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
-\Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t5 _) \Rightarrow t5]))
-(THead k u1 t3) (THead (Flat Appl) w v) H8) in ((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) w v) H8) in (eq_ind K (Flat Appl) (\lambda
-(k0: K).((eq T u1 w) \to ((eq T t3 v) \to ((eq T (THead k0 u2 t4) t2) \to
-((pr0 u1 u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead
-(Bind Abst) u t0))))))))) (\lambda (H13: (eq T u1 w)).(eq_ind T w (\lambda
-(t5: T).((eq T t3 v) \to ((eq T (THead (Flat Appl) u2 t4) t2) \to ((pr0 t5
-u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst)
-u t0)))))))) (\lambda (H14: (eq T t3 v)).(eq_ind T v (\lambda (t5: T).((eq T
-(THead (Flat Appl) u2 t4) t2) \to ((pr0 w u2) \to ((pr0 t5 t4) \to (ty3 g c2
-t2 (THead (Flat Appl) w (THead (Bind Abst) u t0))))))) (\lambda (H15: (eq T
-(THead (Flat Appl) u2 t4) t2)).(eq_ind T (THead (Flat Appl) u2 t4) (\lambda
-(t5: T).((pr0 w u2) \to ((pr0 v t4) \to (ty3 g c2 t5 (THead (Flat Appl) w
-(THead (Bind Abst) u t0)))))) (\lambda (H16: (pr0 w u2)).(\lambda (H17: (pr0
-v t4)).(ex_ind T (\lambda (t5: T).(ty3 g c2 (THead (Bind Abst) u t0) t5))
-(ty3 g c2 (THead (Flat Appl) u2 t4) (THead (Flat Appl) w (THead (Bind Abst) u
-t0))) (\lambda (x: T).(\lambda (H18: (ty3 g c2 (THead (Bind Abst) u t0)
-x)).(ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 c2
-(THead (Bind Abst) u t5) x)))) (\lambda (_: T).(\lambda (t6: T).(\lambda (_:
-T).(ty3 g c2 u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
-(CHead c2 (Bind Abst) u) t0 t5)))) (\lambda (t5: T).(\lambda (_: T).(\lambda
-(t7: T).(ty3 g (CHead c2 (Bind Abst) u) t5 t7)))) (ty3 g c2 (THead (Flat
-Appl) u2 t4) (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c2 (THead (Bind Abst)
-u x0) x)).(\lambda (H20: (ty3 g c2 u x1)).(\lambda (H21: (ty3 g (CHead c2
-(Bind Abst) u) t0 x0)).(\lambda (H22: (ty3 g (CHead c2 (Bind Abst) u) x0
-x2)).(ty3_conv g c2 (THead (Flat Appl) w (THead (Bind Abst) u t0)) (THead
-(Flat Appl) w (THead (Bind Abst) u x0)) (ty3_appl g c2 w u (H1 c2 H4 w
+b0])])) (THead (Bind b0) u0 (lift (S O) O t5)) (THead (Bind b) u t2) H8) in
+(eq_ind B b (\lambda (b1: B).((eq T u0 u) \to ((eq T (lift (S O) O t5) t2)
+\to ((eq T t6 t4) \to ((not (eq B b1 Abst)) \to ((pr0 t5 t6) \to (ty3 g c2 t4
+(THead (Bind b) u t3)))))))) (\lambda (H13: (eq T u0 u)).(eq_ind T u (\lambda
+(_: T).((eq T (lift (S O) O t5) t2) \to ((eq T t6 t4) \to ((not (eq B b
+Abst)) \to ((pr0 t5 t6) \to (ty3 g c2 t4 (THead (Bind b) u t3))))))) (\lambda
+(H14: (eq T (lift (S O) O t5) t2)).(eq_ind T (lift (S O) O t5) (\lambda (_:
+T).((eq T t6 t4) \to ((not (eq B b Abst)) \to ((pr0 t5 t6) \to (ty3 g c2 t4
+(THead (Bind b) u t3)))))) (\lambda (H15: (eq T t6 t4)).(eq_ind T t4 (\lambda
+(t7: T).((not (eq B b Abst)) \to ((pr0 t5 t7) \to (ty3 g c2 t4 (THead (Bind
+b) u t3))))) (\lambda (H16: (not (eq B b Abst))).(\lambda (H17: (pr0 t5
+t4)).(let H18 \def (eq_ind_r T t2 (\lambda (t7: T).(\forall (c3: C).((wcpr0
+(CHead c (Bind b) u) c3) \to (\forall (t8: T).((pr0 t7 t8) \to (ty3 g c3 t8
+t3)))))) H3 (lift (S O) O t5) H14) in (let H19 \def (eq_ind_r T t2 (\lambda
+(t7: T).(ty3 g (CHead c (Bind b) u) t7 t3)) H2 (lift (S O) O t5) H14) in
+(ex_ind T (\lambda (t7: T).(ty3 g (CHead c2 (Bind b) u) t3 t7)) (ty3 g c2 t4
+(THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H20: (ty3 g (CHead c2 (Bind
+b) u) t3 x)).(B_ind (\lambda (b1: B).((not (eq B b1 Abst)) \to ((ty3 g (CHead
+c2 (Bind b1) u) t3 x) \to ((ty3 g (CHead c2 (Bind b1) u) (lift (S O) O t4)
+t3) \to (ty3 g c2 t4 (THead (Bind b1) u t3)))))) (\lambda (H21: (not (eq B
+Abbr Abst))).(\lambda (H22: (ty3 g (CHead c2 (Bind Abbr) u) t3 x)).(\lambda
+(H23: (ty3 g (CHead c2 (Bind Abbr) u) (lift (S O) O t4) t3)).(let H24 \def
+(ty3_gen_cabbr g (CHead c2 (Bind Abbr) u) (lift (S O) O t4) t3 H23 c2 u O
+(getl_refl Abbr c2 u) (CHead c2 (Bind Abbr) u) (csubst1_refl O u (CHead c2
+(Bind Abbr) u)) c2 (drop_drop (Bind Abbr) O c2 c2 (drop_refl c2) u)) in
+(ex3_2_ind T T (\lambda (y1: T).(\lambda (_: T).(subst1 O u (lift (S O) O t4)
+(lift (S O) O y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 O u t3 (lift (S
+O) O y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g c2 y1 y2))) (ty3 g c2 t4
+(THead (Bind Abbr) u t3)) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H25:
+(subst1 O u (lift (S O) O t4) (lift (S O) O x0))).(\lambda (H26: (subst1 O u
+t3 (lift (S O) O x1))).(\lambda (H27: (ty3 g c2 x0 x1)).(let H28 \def (eq_ind
+T x0 (\lambda (t7: T).(ty3 g c2 t7 x1)) H27 t4 (lift_inj x0 t4 (S O) O
+(subst1_gen_lift_eq t4 u (lift (S O) O x0) (S O) O O (le_n O) (eq_ind_r nat
+(plus (S O) O) (\lambda (n: nat).(lt O n)) (le_n (plus (S O) O)) (plus O (S
+O)) (plus_sym O (S O))) H25))) in (ty3_conv g c2 (THead (Bind Abbr) u t3)
+(THead (Bind Abbr) u x) (ty3_bind g c2 u t0 (H1 c2 H4 u (pr0_refl u)) Abbr t3
+x H22) t4 x1 H28 (pc3_pr3_x c2 x1 (THead (Bind Abbr) u t3) (pr3_t (THead
+(Bind Abbr) u (lift (S O) O x1)) (THead (Bind Abbr) u t3) c2 (pr3_pr2 c2
+(THead (Bind Abbr) u t3) (THead (Bind Abbr) u (lift (S O) O x1)) (pr2_free c2
+(THead (Bind Abbr) u t3) (THead (Bind Abbr) u (lift (S O) O x1)) (pr0_delta1
+u u (pr0_refl u) t3 t3 (pr0_refl t3) (lift (S O) O x1) H26))) x1 (pr3_pr2 c2
+(THead (Bind Abbr) u (lift (S O) O x1)) x1 (pr2_free c2 (THead (Bind Abbr) u
+(lift (S O) O x1)) x1 (pr0_zeta Abbr H21 x1 x1 (pr0_refl x1) u))))))))))))
+H24))))) (\lambda (H21: (not (eq B Abst Abst))).(\lambda (_: (ty3 g (CHead c2
+(Bind Abst) u) t3 x)).(\lambda (_: (ty3 g (CHead c2 (Bind Abst) u) (lift (S
+O) O t4) t3)).(let H24 \def (match (H21 (refl_equal B Abst)) in False return
+(\lambda (_: False).(ty3 g c2 t4 (THead (Bind Abst) u t3))) with []) in
+H24)))) (\lambda (H21: (not (eq B Void Abst))).(\lambda (H22: (ty3 g (CHead
+c2 (Bind Void) u) t3 x)).(\lambda (H23: (ty3 g (CHead c2 (Bind Void) u) (lift
+(S O) O t4) t3)).(let H24 \def (ty3_gen_cvoid g (CHead c2 (Bind Void) u)
+(lift (S O) O t4) t3 H23 c2 u O (getl_refl Void c2 u) c2 (drop_drop (Bind
+Void) O c2 c2 (drop_refl c2) u)) in (ex3_2_ind T T (\lambda (y1: T).(\lambda
+(_: T).(eq T (lift (S O) O t4) (lift (S O) O y1)))) (\lambda (_: T).(\lambda
+(y2: T).(eq T t3 (lift (S O) O y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3
+g c2 y1 y2))) (ty3 g c2 t4 (THead (Bind Void) u t3)) (\lambda (x0:
+T).(\lambda (x1: T).(\lambda (H25: (eq T (lift (S O) O t4) (lift (S O) O
+x0))).(\lambda (H26: (eq T t3 (lift (S O) O x1))).(\lambda (H27: (ty3 g c2 x0
+x1)).(let H28 \def (eq_ind T t3 (\lambda (t7: T).(ty3 g (CHead c2 (Bind Void)
+u) t7 x)) H22 (lift (S O) O x1) H26) in (eq_ind_r T (lift (S O) O x1)
+(\lambda (t7: T).(ty3 g c2 t4 (THead (Bind Void) u t7))) (let H29 \def
+(eq_ind_r T x0 (\lambda (t7: T).(ty3 g c2 t7 x1)) H27 t4 (lift_inj t4 x0 (S
+O) O H25)) in (ty3_conv g c2 (THead (Bind Void) u (lift (S O) O x1)) (THead
+(Bind Void) u x) (ty3_bind g c2 u t0 (H1 c2 H4 u (pr0_refl u)) Void (lift (S
+O) O x1) x H28) t4 x1 H29 (pc3_s c2 x1 (THead (Bind Void) u (lift (S O) O
+x1)) (pc3_pr2_r c2 (THead (Bind Void) u (lift (S O) O x1)) x1 (pr2_free c2
+(THead (Bind Void) u (lift (S O) O x1)) x1 (pr0_zeta Void H21 x1 x1 (pr0_refl
+x1) u)))))) t3 H26))))))) H24))))) b H16 H20 (H18 (CHead c2 (Bind b) u)
+(wcpr0_comp c c2 H4 u u (pr0_refl u) (Bind b)) (lift (S O) O t4) (pr0_lift t5
+t4 H17 (S O) O))))) (ty3_correct g (CHead c2 (Bind b) u) (lift (S O) O t4) t3
+(H18 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H4 u u (pr0_refl u) (Bind b))
+(lift (S O) O t4) (pr0_lift t5 t4 H17 (S O) O)))))))) t6 (sym_eq T t6 t4
+H15))) t2 H14)) u0 (sym_eq T u0 u H13))) b0 (sym_eq B b0 b H12))) H11)) H10))
+H9 H6 H7))) | (pr0_tau t5 t6 H6 u0) \Rightarrow (\lambda (H7: (eq T (THead
+(Flat Cast) u0 t5) (THead (Bind b) u t2))).(\lambda (H8: (eq T t6 t4)).((let
+H9 \def (eq_ind T (THead (Flat Cast) u0 t5) (\lambda (e: T).(match e 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 t2) H7) in (False_ind ((eq T t6 t4) \to ((pr0
+t5 t6) \to (ty3 g c2 t4 (THead (Bind b) u t3)))) H9)) H8 H6)))]) in (H6
+(refl_equal T (THead (Bind b) u t2)) (refl_equal T t4)))))))))))))))))
+(\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w
+u)).(\lambda (H1: ((\forall (c2: C).((wcpr0 c c2) \to (\forall (t2: T).((pr0
+w t2) \to (ty3 g c2 t2 u))))))).(\lambda (v: T).(\lambda (t0: T).(\lambda
+(H2: (ty3 g c v (THead (Bind Abst) u t0))).(\lambda (H3: ((\forall (c2:
+C).((wcpr0 c c2) \to (\forall (t2: T).((pr0 v t2) \to (ty3 g c2 t2 (THead
+(Bind Abst) u t0)))))))).(\lambda (c2: C).(\lambda (H4: (wcpr0 c
+c2)).(\lambda (t2: T).(\lambda (H5: (pr0 (THead (Flat Appl) w v) t2)).(let H6
+\def (match H5 in pr0 return (\lambda (t3: T).(\lambda (t4: T).(\lambda (_:
+(pr0 t3 t4)).((eq T t3 (THead (Flat Appl) w v)) \to ((eq T t4 t2) \to (ty3 g
+c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))))) with [(pr0_refl
+t3) \Rightarrow (\lambda (H6: (eq T t3 (THead (Flat Appl) w v))).(\lambda
+(H7: (eq T t3 t2)).(eq_ind T (THead (Flat Appl) w v) (\lambda (t4: T).((eq T
+t4 t2) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))
+(\lambda (H8: (eq T (THead (Flat Appl) w v) t2)).(eq_ind T (THead (Flat Appl)
+w v) (\lambda (t4: T).(ty3 g c2 t4 (THead (Flat Appl) w (THead (Bind Abst) u
+t0)))) (ty3_appl g c2 w u (H1 c2 H4 w (pr0_refl w)) v t0 (H3 c2 H4 v
+(pr0_refl v))) t2 H8)) t3 (sym_eq T t3 (THead (Flat Appl) w v) H6) H7))) |
+(pr0_comp u1 u2 H6 t3 t4 H7 k) \Rightarrow (\lambda (H8: (eq T (THead k u1
+t3) (THead (Flat Appl) w v))).(\lambda (H9: (eq T (THead k u2 t4) t2)).((let
+H10 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
+with [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t5)
+\Rightarrow t5])) (THead k u1 t3) (THead (Flat Appl) w v) H8) in ((let H11
+\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
+with [(TSort _) \Rightarrow u1 | (TLRef _) \Rightarrow u1 | (THead _ t5 _)
+\Rightarrow t5])) (THead k u1 t3) (THead (Flat Appl) w v) H8) in ((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) w v) H8) in (eq_ind K
+(Flat Appl) (\lambda (k0: K).((eq T u1 w) \to ((eq T t3 v) \to ((eq T (THead
+k0 u2 t4) t2) \to ((pr0 u1 u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat
+Appl) w (THead (Bind Abst) u t0))))))))) (\lambda (H13: (eq T u1 w)).(eq_ind
+T w (\lambda (t5: T).((eq T t3 v) \to ((eq T (THead (Flat Appl) u2 t4) t2)
+\to ((pr0 t5 u2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w
+(THead (Bind Abst) u t0)))))))) (\lambda (H14: (eq T t3 v)).(eq_ind T v
+(\lambda (t5: T).((eq T (THead (Flat Appl) u2 t4) t2) \to ((pr0 w u2) \to
+((pr0 t5 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u
+t0))))))) (\lambda (H15: (eq T (THead (Flat Appl) u2 t4) t2)).(eq_ind T
+(THead (Flat Appl) u2 t4) (\lambda (t5: T).((pr0 w u2) \to ((pr0 v t4) \to
+(ty3 g c2 t5 (THead (Flat Appl) w (THead (Bind Abst) u t0)))))) (\lambda
+(H16: (pr0 w u2)).(\lambda (H17: (pr0 v t4)).(ex_ind T (\lambda (t5: T).(ty3
+g c2 (THead (Bind Abst) u t0) t5)) (ty3 g c2 (THead (Flat Appl) u2 t4) (THead
+(Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x: T).(\lambda (H18: (ty3
+g c2 (THead (Bind Abst) u t0) x)).(ex3_2_ind T T (\lambda (t5: T).(\lambda
+(_: T).(pc3 c2 (THead (Bind Abst) u t5) x))) (\lambda (_: T).(\lambda (t6:
+T).(ty3 g c2 u t6))) (\lambda (t5: T).(\lambda (_: T).(ty3 g (CHead c2 (Bind
+Abst) u) t0 t5))) (ty3 g c2 (THead (Flat Appl) u2 t4) (THead (Flat Appl) w
+(THead (Bind Abst) u t0))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (_:
+(pc3 c2 (THead (Bind Abst) u x0) x)).(\lambda (H20: (ty3 g c2 u x1)).(\lambda
+(H21: (ty3 g (CHead c2 (Bind Abst) u) t0 x0)).(ty3_conv g c2 (THead (Flat
+Appl) w (THead (Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u
+x0)) (ty3_appl g c2 w u (H1 c2 H4 w (pr0_refl w)) (THead (Bind Abst) u t0) x0
+(ty3_bind g c2 u x1 H20 Abst t0 x0 H21)) (THead (Flat Appl) u2 t4) (THead
+(Flat Appl) u2 (THead (Bind Abst) u t0)) (ty3_appl g c2 u2 u (H1 c2 H4 u2
+H16) t4 t0 (H3 c2 H4 t4 H17)) (pc3_pr2_x c2 (THead (Flat Appl) u2 (THead
+(Bind Abst) u t0)) (THead (Flat Appl) w (THead (Bind Abst) u t0)) (pr2_head_1
+c2 w u2 (pr2_free c2 w u2 H16) (Flat Appl) (THead (Bind Abst) u t0)))))))))
+(ty3_gen_bind g Abst c2 u t0 x H18)))) (ty3_correct g c2 v (THead (Bind Abst)
+u t0) (H3 c2 H4 v (pr0_refl v)))))) t2 H15)) t3 (sym_eq T t3 v H14))) u1
+(sym_eq T u1 w H13))) k (sym_eq K k (Flat Appl) H12))) H11)) H10)) H9 H6
+H7))) | (pr0_beta u0 v1 v2 H6 t3 t4 H7) \Rightarrow (\lambda (H8: (eq T
+(THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Flat Appl) w
+v))).(\lambda (H9: (eq T (THead (Bind Abbr) v2 t4) t2)).((let H10 \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 _ _ t5) \Rightarrow t5])) (THead (Flat
+Appl) v1 (THead (Bind Abst) u0 t3)) (THead (Flat Appl) w v) H8) in ((let H11
+\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
+with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 | (THead _ t5 _)
+\Rightarrow t5])) (THead (Flat Appl) v1 (THead (Bind Abst) u0 t3)) (THead
+(Flat Appl) w v) H8) in (eq_ind T w (\lambda (t5: T).((eq T (THead (Bind
+Abst) u0 t3) v) \to ((eq T (THead (Bind Abbr) v2 t4) t2) \to ((pr0 t5 v2) \to
+((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w (THead (Bind Abst) u
+t0)))))))) (\lambda (H12: (eq T (THead (Bind Abst) u0 t3) v)).(eq_ind T
+(THead (Bind Abst) u0 t3) (\lambda (_: T).((eq T (THead (Bind Abbr) v2 t4)
+t2) \to ((pr0 w v2) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w
+(THead (Bind Abst) u t0))))))) (\lambda (H13: (eq T (THead (Bind Abbr) v2 t4)
+t2)).(eq_ind T (THead (Bind Abbr) v2 t4) (\lambda (t5: T).((pr0 w v2) \to
+((pr0 t3 t4) \to (ty3 g c2 t5 (THead (Flat Appl) w (THead (Bind Abst) u
+t0)))))) (\lambda (H14: (pr0 w v2)).(\lambda (H15: (pr0 t3 t4)).(let H16 \def
+(eq_ind_r T v (\lambda (t5: T).(\forall (c3: C).((wcpr0 c c3) \to (\forall
+(t6: T).((pr0 t5 t6) \to (ty3 g c3 t6 (THead (Bind Abst) u t0))))))) H3
+(THead (Bind Abst) u0 t3) H12) in (let H17 \def (eq_ind_r T v (\lambda (t5:
+T).(ty3 g c t5 (THead (Bind Abst) u t0))) H2 (THead (Bind Abst) u0 t3) H12)
+in (ex_ind T (\lambda (t5: T).(ty3 g c2 (THead (Bind Abst) u t0) t5)) (ty3 g
+c2 (THead (Bind Abbr) v2 t4) (THead (Flat Appl) w (THead (Bind Abst) u t0)))
+(\lambda (x: T).(\lambda (H18: (ty3 g c2 (THead (Bind Abst) u t0)
+x)).(ex3_2_ind T T (\lambda (t5: T).(\lambda (_: T).(pc3 c2 (THead (Bind
+Abst) u t5) x))) (\lambda (_: T).(\lambda (t6: T).(ty3 g c2 u t6))) (\lambda
+(t5: T).(\lambda (_: T).(ty3 g (CHead c2 (Bind Abst) u) t0 t5))) (ty3 g c2
+(THead (Bind Abbr) v2 t4) (THead (Flat Appl) w (THead (Bind Abst) u t0)))
+(\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 c2 (THead (Bind Abst) u
+x0) x)).(\lambda (H20: (ty3 g c2 u x1)).(\lambda (H21: (ty3 g (CHead c2 (Bind
+Abst) u) t0 x0)).(ex3_2_ind T T (\lambda (t5: T).(\lambda (_: T).(pc3 c2
+(THead (Bind Abst) u0 t5) (THead (Bind Abst) u t0)))) (\lambda (_:
+T).(\lambda (t6: T).(ty3 g c2 u0 t6))) (\lambda (t5: T).(\lambda (_: T).(ty3
+g (CHead c2 (Bind Abst) u0) t4 t5))) (ty3 g c2 (THead (Bind Abbr) v2 t4)
+(THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x2: T).(\lambda
+(x3: T).(\lambda (H22: (pc3 c2 (THead (Bind Abst) u0 x2) (THead (Bind Abst) u
+t0))).(\lambda (H23: (ty3 g c2 u0 x3)).(\lambda (H24: (ty3 g (CHead c2 (Bind
+Abst) u0) t4 x2)).(land_ind (pc3 c2 u0 u) (\forall (b: B).(\forall (u1:
+T).(pc3 (CHead c2 (Bind b) u1) x2 t0))) (ty3 g c2 (THead (Bind Abbr) v2 t4)
+(THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (H25: (pc3 c2 u0
+u)).(\lambda (H26: ((\forall (b: B).(\forall (u1: T).(pc3 (CHead c2 (Bind b)
+u1) x2 t0))))).(ty3_conv g c2 (THead (Flat Appl) w (THead (Bind Abst) u t0))
+(THead (Flat Appl) w (THead (Bind Abst) u x0)) (ty3_appl g c2 w u (H1 c2 H4 w