proposition: Lemma isassocisof {X Y : setwithbinop} (f : binopiso X Y) (is : isassoc (@op X)) : isassoc (@op Y).
proof: Proof. apply (isassocmonob (invbinopiso f) is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions