Generalize the definition of Subset

[tonyxty]

Subsets are currently only defined for Monoids:

arend-lib/src/Algebra/Ring/Localization.ard

Lines 23 to 32 in 6be71a0

	-- | A subset of a monoid.
	\class Subset (M : Monoid)
	| \fix 8 contains : M -> \Prop
	\instance SubsetPoset {M : Monoid} : Poset (Subset M)
	| <= (S S' : Subset M) => \Pi (x : M) -> S.contains x -> S'.contains x
	| <=-reflexive x p => p
	| <=-transitive S1<=S2 S2<=S3 x p => S2<=S3 x (S1<=S2 x p)
	| <=-antisymmetric S1<=S2 S2<=S1 => path (\lam i => \new Subset M (\lam x => propExt (S1<=S2 x) (S2<=S1 x) @ i))

while they can be defined for BaseSets. It goes without saying that this is useful in general.