- matitaInit matitaprover matitadep matitamake:

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

diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
index 4f117d302d316a6b686f1d22325cbac16e110862..c8f4922b15a96474648c322feae0d342550d2ef9 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
+++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
@@ -26,9 +26,13 @@ include "wcpr0/fwd.ma".
 
 include "pr3/wcpr0.ma".
 
+include "ex2/props.ma".
+
 include "ex1/props.ma".
 
 include "ty3/tau0.ma".
 
+include "ty3/nf2.ma".
+
 include "ty3/dec.ma".