X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Ftheory.ma;h=daf2a250e29990fce62e1077fad4b3b6a7811b41;hb=b58315ef220a130a44acbf528cd6885ddadad642;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..daf2a250e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
@@ -20,15 +20,19 @@ include "subst0/tlt.ma".
 
 include "tau1/cnt.ma".
 
-include "gz/props.ma".
+include "ex0/props.ma".
 
 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".