proposition: Lemma isapropisbinopfun {X Y : setwithbinop} (f : X -> Y) : isaprop (isbinopfun f).
proof: Proof. apply impred. intro x. apply impred. intro x'. apply (setproperty Y). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions