People, I think of implementing Subsetoid, Subsemigroup, Subgroup ..., by using an injective \~~-conrguent map, using Function.Injection.Injection and a membership predicate. At least, SubDecSetoid is compiled. But for any occasion, may be, these Sub- guys are in Standard library? Thanks, ------ Sergei