dependences fixed

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / theory.ma

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 c24e6622d24f863094b0405ccafad34f8ff17123..c0b188265a421764443a20860b5c4f7847f47fe9 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
@@ -74,6 +74,10 @@ include "drop/fwd.ma".
 
 include "drop/props.ma".
 
+include "drop1/defs.ma".
+
+include "drop1/props.ma".
+
 include "G/defs.ma".
 
 include "next_plus/defs.ma".