X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Flift%2Fdefs.ma;h=66b000e77f1463c1ee7a8ccbebc6ecf4f0c0b1fc;hb=9408f2869ddbbbae68dcb23ebf6c358c61888d0d;hp=41c5d1e464981bb0ee3f6530dfa4368658d70d02;hpb=963b07897f7548007c076c465c7f6733df481419;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma
index 41c5d1e46..66b000e77 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma
@@ -18,6 +18,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs".
 
 include "T/defs.ma".
 
+include "tlist/defs.ma".
+
 include "s/defs.ma".
 
 definition lref_map: