i v c1 c0)).(or3_intro2 (land (eq C c1 c0) (subst0 i v t1 t0)) (land (eq T t1
t0) (csubst0 i v c1 c0)) (land (subst0 i v t1 t0) (csubst0 i v c1 c0)) (conj
(subst0 i v t1 t0) (csubst0 i v c1 c0) H0 H1)))))) c2 t2 H))))))).
i v c1 c0)).(or3_intro2 (land (eq C c1 c0) (subst0 i v t1 t0)) (land (eq T t1
t0) (csubst0 i v c1 c0)) (land (subst0 i v t1 t0) (csubst0 i v c1 c0)) (conj
(subst0 i v t1 t0) (csubst0 i v c1 c0) H0 H1)))))) c2 t2 H))))))).