(\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda
(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:
+(CHead c (Bind Abst) x0) x1 x4)).(land_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: