Definition setwithbinopquot {X : setwithbinop} (R : binopeqrel X) : setwithbinop. Proof. exists (setquotinset R). set (qt := setquot R). set (qtset := setquotinset R). assert (iscomp : iscomprelrelfun2 R R op) by apply (iscompbinoptransrel R (eqreltrans R) (pr2 R)). set (qtmlt := setquotfun2 R R op iscomp). simpl. unfold binop. apply qtmlt. Defined.