proposition: Lemma isapropissubmonoid {X : monoid} (A : hsubtype X) : isaprop (issubmonoid A).
proof: Proof. apply (isofhleveldirprod 1). - apply isapropissubsetwithbinop. - apply (pr2 (A (unel X))). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders