\forall (u2: T).(\forall (t3: T).(\forall (w: T).((subst0 O u2 t3 w) \to
(\forall (u3: T).(\forall (t5: T).(\forall (w0: T).((subst0 O u3 t5 w0) \to
(\forall (x: T).((pr0 u2 x) \to ((pr0 u3 x) \to (\forall (x0: T).((pr0 t3 x0)
\forall (u2: T).(\forall (t3: T).(\forall (w: T).((subst0 O u2 t3 w) \to
(\forall (u3: T).(\forall (t5: T).(\forall (w0: T).((subst0 O u3 t5 w0) \to
(\forall (x: T).((pr0 u2 x) \to ((pr0 u3 x) \to (\forall (x0: T).((pr0 t3 x0)