\forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (t1:
T).(\forall (t2: T).((pr3 c1 t1 t2) \to (pr3 c2 t1 t2))))))
\def
\forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (t1:
T).(\forall (t2: T).((pr3 c1 t1 t2) \to (pr3 c2 t1 t2))))))
\def