proposition: Lemma setquotfun2_equal {X Y Z} (RX:eqrel X) (RY:eqrel Y) (RZ:eqrel Z) (f:X->Y->Z) (is:iscomprelrelfun2' RX RY RZ f) (x:X) (y:Y) : setquotfun2' f is (setquotpr RX x) (setquotpr RY y) = setquotpr RZ (f x y).
proof: Proof. reflexivity. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA