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=423565e498d6271d03449a17c770e857b4fb932e;hb=ac51c1272a969de33bb3fcf75aa4c6e3f56d1721;hp=405f95aff0dc033084bbee5f073d384de3d05945;hpb=bfb39a9bcb10b87ab7d6e09928fb82d340d8feca;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 405f95aff..423565e49 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
@@ -176,5 +176,35 @@ include "aplus/props.ma".
 
 include "leq/defs.ma".
 
+include "leq/fwd.ma".
+
+include "leq/props.ma".
+
 include "leq/asucc.ma".
 
+include "llt/defs.ma".
+
+include "llt/props.ma".
+
+include "aprem/defs.ma".
+
+include "aprem/props.ma".
+
+include "gz/defs.ma".
+
+include "gz/props.ma".
+
+include "arity/defs.ma".
+
+include "arity/fwd.ma".
+
+include "arity/props.ma".
+
+include "arity/subst0.ma".
+
+include "arity/lift1.ma".
+
+include "arity/cimp.ma".
+
+include "arity/aprem.ma".
+