\forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall
(v: T).((getl i c1 (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2:
C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda
\forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall
(v: T).((getl i c1 (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2:
C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda