X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Flift%2Ftlt.ma;h=b67722f58eca72d17f85f8253d96291c8a825580;hb=260615773f01b051db400034a8df7c578fe53718;hp=9ce6a4755689149bdf4a3a063c9845f4d12d7daa;hpb=205276c80f0c39fe46bf2b9b7811b3343eb5c0d5;p=helm.git

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 9ce6a4755..b67722f58 100644
--- 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