X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL%2FZah%2Fsetoid.ma;h=e30b5a205723b3ae8cbad46098bdb2d1edc99989;hb=2b95f946837707c6ad30d1b8317d73c55cda3dc8;hp=8815ee5bb6e3bbc0314c1aa95dcca55d28fe4c18;hpb=37900b93fb87f68fefa0814abe24a123a4d20e02;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma b/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
index 8815ee5bb..e30b5a205 100644
--- a/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
+++ b/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/Zah/setoid".
 
-include "NPlus/props.ma".
+include "NPlus/monoid.ma".
 include "Zah/defs.ma".
 
 theorem nplus_total: \forall p,q. \exists r. p + q == r.
@@ -57,4 +57,4 @@ theorem zeq_trans: \forall z1,z2. z1 = z2 \to
  
  
 
-*)
\ No newline at end of file
+*)