(* This file was automatically generated: do not edit *********************)
-include "csubst1/defs.ma".
+include "LambdaDelta-1/csubst1/defs.ma".
-include "csubst0/fwd.ma".
+include "LambdaDelta-1/csubst0/fwd.ma".
-include "subst1/props.ma".
+include "LambdaDelta-1/subst1/props.ma".
theorem csubst1_gen_head:
\forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).(\forall