Lemma weqldistrrdistr {X : hSet} (opp1 opp2 : binop X) (is : iscomm opp2) : (isldistr opp1 opp2) ≃ (isrdistr opp1 opp2). Proof. assert (f : (isldistr opp1 opp2) → (isrdistr opp1 opp2)). { unfold isldistr. unfold isrdistr. intro isl. intros x x' x''. induction (is x'' (opp1 x x')). induction (is x'' x). induction (is x'' x'). apply (isl x x' x''). } assert (g : (isrdistr opp1 opp2) → (isldistr opp1 opp2)). { unfold isldistr. unfold isrdistr. intro isr. intros x x' x''. induction (is (opp1 x x') x''). induction (is x x''). induction (is x' x''). apply (isr x x' x''). } exists f. apply (isweqimplimpl f g (isapropisldistr opp1 opp2) (isapropisrdistr opp1 opp2)). Defined.