\forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (t2: T).(\forall
(v: T).(\forall (i: nat).((fsubst0 i v c1 t1 c2 t2) \to (or3 (land (eq C c1
c2) (subst0 i v t1 t2)) (land (eq T t1 t2) (csubst0 i v c1 c2)) (land (subst0
\forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (t2: T).(\forall
(v: T).(\forall (i: nat).((fsubst0 i v c1 t1 c2 t2) \to (or3 (land (eq C c1
c2) (subst0 i v t1 t2)) (land (eq T t1 t2) (csubst0 i v c1 c2)) (land (subst0