]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
new theorems
[helm.git] / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / theory.ma
index 5e6b423f75b46fc6d3a9a69f7595ae8a32217e08..c24e6622d24f863094b0405ccafad34f8ff17123 100644 (file)
@@ -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".