(* This file was automatically generated: do not edit *********************)
-
-
-include "fsubst0/defs.ma".
+include "LambdaDelta-1/fsubst0/defs.ma".
theorem fsubst0_gen_base:
\forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (t2: T).(\forall