\forall (c: C).(\forall (u1: T).(\forall (u2: T).(\forall (t1: T).(\forall
(t2: T).((pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)) \to
(land (pc3 c u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u)
\forall (c: C).(\forall (u1: T).(\forall (u2: T).(\forall (t1: T).(\forall
(t2: T).((pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)) \to
(land (pc3 c u1 u2) (\forall (b: B).(\forall (u: T).(pc3 (CHead c (Bind b) u)