\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
a) \to ((nf2 c t) \to (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u: T).(eq T t
(THead (Bind Abst) w u)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w)))
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
a) \to ((nf2 c t) \to (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u: T).(eq T t
(THead (Bind Abst) w u)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w)))