proposition: Lemma isinvisob {X Y : setwithbinop} (f : binopiso X Y) (uny : Y) (invy : Y -> Y) (is : isinv (@op Y) uny invy) : isinv (@op X) (invmap (pr1 f) uny) (funcomp (pr1 f) (funcomp invy (invmap (pr1 f)))).
proof: Proof. apply (isinvisof (invbinopiso f) uny invy is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions