-(H18: (pc3 c x0 w)).(\lambda (H19: ((\forall (b: B).(\forall (u0: T).(pc3
-(CHead c (Bind b) u0) x5 u))))).(let H_y \def (pc3_nf2 c x0 w H18 H6 H1) in
-(let H20 \def (eq_ind T x0 (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) t0)
-x1 x5)) H16 w H_y) in (let H21 \def (eq_ind T x0 (\lambda (t0: T).(nf2 (CHead
-c (Bind Abst) t0) x1)) H7 w H_y) in (eq_ind_r T w (\lambda (t0: T).(ex4_2 T T
-(\lambda (v: T).(\lambda (_: T).(eq T (THead (Bind Abst) t0 x1) (THead (Bind
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v:
-T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v:
-T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))))) (ex4_2_intro T T
-(\lambda (v: T).(\lambda (_: T).(eq T (THead (Bind Abst) w x1) (THead (Bind
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v:
-T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v:
-T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))) x1 x3 (refl_equal T
-(THead (Bind Abst) w x1)) H11 (ty3_conv g (CHead c (Bind Abst) w) u x2 H12 x1
-x5 H20 (H19 Abst w)) H21) x0 H_y)))))) (pc3_gen_abst c x0 w x5 u H14)))))))))
-(ty3_gen_bind g Abst c x0 x1 (THead (Bind Abst) w u) H8)))))))))
-(ty3_gen_bind g Abst c w u x H9)))) (ty3_correct g c (THead (Bind Abst) x0
-x1) (THead (Bind Abst) w u) H8)) t H5))))))) H4)) (\lambda (H4: (ex nat
-(\lambda (n: nat).(eq T t (TSort n))))).(ex_ind nat (\lambda (n: nat).(eq T t
-(TSort n))) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T t (THead (Bind
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v:
-T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v:
-T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda (x:
-nat).(\lambda (H5: (eq T t (TSort x))).(let H6 \def (eq_ind T t (\lambda (t0:
-T).(ty3 g c t0 (THead (Bind Abst) w u))) H (TSort x) H5) in (eq_ind_r T
-(TSort x) (\lambda (t0: T).(ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T
-t0 (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w
-w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u)))
-(\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))))
-(pc3_gen_sort_abst c w u (next g x) (ty3_gen_sort g c (THead (Bind Abst) w u)
-x H6) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (TSort x) (THead (Bind
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v:
+(x4: T).(\lambda (x5: T).(\lambda (H13: (pc3 c (THead (Bind Abst) x0 x4)
+(THead (Bind Abst) w u))).(\lambda (_: (ty3 g c x0 x5)).(\lambda (H15: (ty3 g
+(CHead c (Bind Abst) x0) x1 x4)).(and_ind (pc3 c x0 w) (\forall (b:
+B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x4 u))) (ex4_2 T T (\lambda
+(v: T).(\lambda (_: T).(eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w
+v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: