\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u: T).((pc3 c t
(THead (Bind Abst) w u)) \to (\forall (v: T).((pc3 c v w) \to (pc3 c (THead
(Bind Abst) v (THead (Flat Appl) (TLRef O) (lift (S O) O t))) t)))))))
\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u: T).((pc3 c t
(THead (Bind Abst) w u)) \to (\forall (v: T).((pc3 c v w) \to (pc3 c (THead
(Bind Abst) v (THead (Flat Appl) (TLRef O) (lift (S O) O t))) t)))))))