\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
a) \to (\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c (CHead d
(Bind Void) u)) \to (ex T (\lambda (v: T).(eq T t (lift (S O) i v))))))))))))
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
a) \to (\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c (CHead d
(Bind Void) u)) \to (ex T (\lambda (v: T).(eq T t (lift (S O) i v))))))))))))