proposition: Lemma isapropissubmodule {R : ring} {M : module R} (A : hsubtype M) : isaprop (issubmodule A).
proof: Proof. intros. apply (isofhleveldirprod 1). - apply isapropissubgr. - apply impred. intro x. apply impred. intro m. apply impred. intro a. apply (pr2 (A _)). Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.Algebra.RigsAndRings UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.Modules.Core