X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Ftheory.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Ftheory.ma;h=c24e6622d24f863094b0405ccafad34f8ff17123;hb=b6c399fc59c61c1071c942f539fabda4d74bb922;hp=5e6b423f75b46fc6d3a9a69f7595ae8a32217e08;hpb=456f7d82d3cf6732daa36bb07d06c23c4a60beda;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 5e6b423f7..c24e6622d 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,54 @@ include "s/defs.ma".
 
 include "s/props.ma".
 
+include "tlt/defs.ma".
+
+include "tlt/props.ma".
+
+include "iso/defs.ma".
+
+include "iso/fwd.ma".
+
+include "iso/props.ma".
+
+include "C/defs.ma".
+
+include "C/props.ma".
+
+include "r/defs.ma".
+
+include "r/props.ma".
+
+include "clen/defs.ma".
+
+include "flt/defs.ma".
+
+include "flt/props.ma".
+
+include "lift/defs.ma".
+
+include "lift/fwd.ma".
+
+include "lift/props.ma".
+
+include "lift/tlt.ma".
+
+include "lift1/defs.ma".
+
+include "lift1/fwd.ma".
+
+include "lift1/props.ma".
+
+include "cnt/defs.ma".
+
+include "cnt/props.ma".
+
+include "drop/defs.ma".
+
+include "drop/fwd.ma".
+
+include "drop/props.ma".
+
 include "G/defs.ma".
 
 include "next_plus/defs.ma".