- some new auxiliary lemmas

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

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 4f117d302d316a6b686f1d22325cbac16e110862..daf2a250e29990fce62e1077fad4b3b6a7811b41 100644 (file)
--- 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".