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_comm O (S O))) H25))) in (ty3_conv g c2 (THead (Bind Abbr) u t3)
+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 (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)).(and_ind (pc3 c2 u0 u) (\forall (b: B).(\forall (u1:
+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)