X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fsubset_inclusion.ma;h=68eba7c1bb7761337cc38bf849a29b3dc41ab6f5;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=6f2e5c9b7895db083e22c18d438720ea4e67d7e1;hpb=c8ba3d001893666a52c393d9cf8a0929dacd007a;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