X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Ftheory.ma;h=b632ec9d488dee5b0f56c43e9fbdb3ff647b6e76;hb=9408f2869ddbbbae68dcb23ebf6c358c61888d0d;hp=2c1ae46cce58b41dac53a8d5765b5049f16c8dfc;hpb=cca52355d183a00695b9e310b17c8945ae915b64;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
index 2c1ae46cc..b632ec9d4 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
@@ -26,6 +26,10 @@ include "s/defs.ma".
 
 include "s/props.ma".
 
+include "tlist/defs.ma".
+
+include "tlist/props.ma".
+
 include "tlt/defs.ma".
 
 include "tlt/props.ma".
@@ -310,9 +314,21 @@ include "sc3/defs.ma".
 
 include "sc3/props.ma".
 
-include "ceqc/defs.ma".
+include "csubc/defs.ma".
+
+include "csubc/props.ma".
+
+include "csubc/csuba.ma".
+
+include "csubc/drop.ma".
+
+include "csubc/drop1.ma".
+
+include "csubc/clear.ma".
+
+include "csubc/getl.ma".
 
-include "ceqc/props.ma".
+include "csubc/arity.ma".
 
 include "sc3/arity.ma".
 
@@ -346,21 +362,21 @@ include "ty3/fsubst0.ma".
 
 include "ty3/subst1.ma".
 
-include "csub3/defs.ma".
+include "csubt/defs.ma".
 
-include "csub3/fwd.ma".
+include "csubt/fwd.ma".
 
-include "csub3/props.ma".
+include "csubt/props.ma".
 
-include "csub3/clear.ma".
+include "csubt/clear.ma".
 
-include "csub3/drop.ma".
+include "csubt/drop.ma".
 
-include "csub3/getl.ma".
+include "csubt/getl.ma".
 
-include "csub3/pc3.ma".
+include "csubt/pc3.ma".
 
-include "csub3/ty3.ma".
+include "csubt/ty3.ma".
 
 include "ty3/pr3.ma".