X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fcnt%2Fprops.ma;h=a33870137ceea84afab8769b29ca7df0cf31fa0e;hb=00305d361464ea4c1c071b9be29482198d521eda;hp=685b59683601e9eca3314f4b08eae56ac1fbeb2e;hpb=01cd30e9b0e915304b3ffef48a0477c69ce7a959;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma
index 685b59683..a33870137 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props".
 
 include "cnt/defs.ma".
 
-include "lift/defs.ma".
+include "lift/fwd.ma".
 
 theorem cnt_lift:
  \forall (t: T).((cnt t) \to (\forall (i: nat).(\forall (d: nat).(cnt (lift i