]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / subset_inclusion.ma
index 6f2e5c9b7895db083e22c18d438720ea4e67d7e1..68eba7c1bb7761337cc38bf849a29b3dc41ab6f5 100644 (file)
@@ -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