proposition: Lemma isapropisdistr {X : hSet} (opp1 opp2 : binop X) : isaprop (isdistr opp1 opp2).
proof: Proof. apply (isofhleveldirprod 1 _ _ (isapropisldistr _ _) (isapropisrdistr _ _)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions