(* This file was automatically generated: do not edit *********************)
-include "csubst0/fwd.ma".
+include "LambdaDelta-1/csubst0/fwd.ma".
-include "drop/fwd.ma".
+include "LambdaDelta-1/drop/fwd.ma".
-include "s/props.ma".
+include "LambdaDelta-1/s/props.ma".
theorem csubst0_drop_gt:
\forall (n: nat).(\forall (i: nat).((lt i n) \to (\forall (c1: C).(\forall