dependences fixed

[helm.git] / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / lift / tlt.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma
index 9ce6a4755689149bdf4a3a063c9845f4d12d7daa..b67722f58eca72d17f85f8253d96291c8a825580 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma
@@ -16,9 +16,9 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt".
 
-include "lift/defs.ma".
+include "lift/fwd.ma".
 
-include "tlt/defs.ma".
+include "tlt/props.ma".
 
 theorem lift_weight_map:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to