proposition: Lemma isrdistrisof {X Y : setwith2binop} (f : twobinopiso X Y) (is : isrdistr (@op1 X) (@op2 X)) : isrdistr (@op1 Y) (@op2 Y).
proof: Proof. apply (isrdistrisob (invtwobinopiso f) is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions