\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(THead (Bind Abbr) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
(t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
(THead (Bind Abbr) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
(t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: