(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/cnt/defs.ma".
-
-include "cnt/defs.ma".
-
-include "lift/fwd.ma".
+include "LambdaDelta-1/lift/fwd.ma".
theorem cnt_lift:
\forall (t: T).((cnt t) \to (\forall (i: nat).(\forall (d: nat).(cnt (lift i