X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Ftheory.ma;h=c8f4922b15a96474648c322feae0d342550d2ef9;hb=09c8bb55c25143efdfbd34a20bb2fe6b681760b6;hp=4f117d302d316a6b686f1d22325cbac16e110862;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
index 4f117d302..c8f4922b1 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
+++ b/helm/software/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".