proposition: Lemma isapropissubgr {X : gr} (A : hsubtype X) : isaprop (issubgr A).
proof: Proof. apply (isofhleveldirprod 1). - apply isapropissubmonoid. - apply impred. intro x. apply impred. intro a. apply (pr2 (A (grinv X x))). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids