(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
(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