proposition: Lemma isapropisassoc {X : hSet} (opp : binop X) : isaprop (isassoc opp).
proof: Proof. apply impred. intro x. apply impred. intro x'. apply impred. intro x''. simpl. apply (setproperty X). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions