(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/lift/fwd.ma".
-
-include "lift/fwd.ma".
-
-include "tlt/props.ma".
+include "LambdaDelta-1/tlt/props.ma".
theorem lift_weight_map:
\forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to