\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (v: T).((ty3 g c u
v) \to (\forall (t1: T).(\forall (t2: T).((ty3 g (CHead c (Bind Abst) v) t1
t2) \to (ty3 g (CHead c (Bind Abbr) u) t1 t2))))))))
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (v: T).((ty3 g c u
v) \to (\forall (t1: T).(\forall (t2: T).((ty3 g (CHead c (Bind Abst) v) t1
t2) \to (ty3 g (CHead c (Bind Abbr) u) t1 t2))))))))