X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fsubset_inclusion.ma;h=68eba7c1bb7761337cc38bf849a29b3dc41ab6f5;hb=6f1b6f85a78d4c8da42f035f433fe4b85962bd9b;hp=6f2e5c9b7895db083e22c18d438720ea4e67d7e1;hpb=2e4a7c54ef77c10cb1cef4b59518c473245ea935;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma
index 6f2e5c9b7..68eba7c1b 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma
@@ -16,7 +16,7 @@ include "ground/lib/subset.ma".
 
 (* INCLUSION FOR SUBSETS ****************************************************)
 
-definition subset_le (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝
+definition subset_le (A): relation2 (𝒫❨A❩) (𝒫❨A❩) ≝
            λu1,u2. ∀p. p ϵ u1 → p ϵ u2.
 
 interpretation