proposition: Lemma isapropisabsorb {X : hSet} (opp1 opp2 : binop X) : isaprop (isabsorb opp1 opp2).
proof: Proof. apply impred_isaprop ; intros x. apply impred_isaprop ; intros y. apply (setproperty X). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions