Lemma isapropisrdistr {X : hSet} (opp1 opp2 : binop X) : isaprop (isrdistr opp1 opp2). Proof. apply impred. intro x. apply impred. intro x'. apply impred. intro x''. simpl. apply (setproperty X). Defined.