proposition: Lemma isgrop_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) : isgrop opp → isgrop (binop_weq_bck H opp).
proof: Proof. intro is. use tpair. apply ismonoidop_weq_bck, (pr1 is). apply invstruct_weq_bck, (pr2 is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions