\forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d x)) \to (ex3_2 T
T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda
\forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d x)) \to (ex3_2 T
T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda