Lemma isapropisringops {X : hSet} (opp1 opp2 : binop X) : isaprop (isringops opp1 opp2). Proof. apply (isofhleveldirprod 1). - apply (isofhleveldirprod 1). + apply isapropisabgrop. + apply isapropismonoidop. - apply isapropisdistr. Defined.