\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
(THead (Flat Appl) u1 t1) x) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
(t2: T).(eq T x (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
\forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
(THead (Flat Appl) u1 t1) x) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
(t2: T).(eq T x (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: