(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/fsubst0/defs.ma".
+include "Basic-1/fsubst0/defs.ma".
theorem fsubst0_gen_base:
\forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (t2: T).(\forall
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))))))).
+(* COMMENTS
+Initial nodes: 431
+END *)