X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Ftheory.ma;h=8b96936ab016f1bea87eb25dc1e30c1b4a2d9ed2;hb=fae18970c0d8e5a9bfab4a740da89bb6caf24ef9;hp=405f95aff0dc033084bbee5f073d384de3d05945;hpb=73663b52b3e1d8ed2f5936177bcc13b6e6b69997;p=helm.git

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 405f95aff..8b96936ab 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
@@ -176,5 +176,7 @@ include "aplus/props.ma".
 
 include "leq/defs.ma".
 
+include "leq/props.ma".
+
 include "leq/asucc.ma".