proposition: Lemma iscomm_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) : iscomm opp → iscomm (binop_weq_bck H opp).
proof: Proof. intros is x y. unfold binop_weq_bck. apply maponpaths, is. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions