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. reflexivity. Defined.
Require Import