Lemma isasetbinopiso (X Y : setwithbinop) : isaset (binopiso X Y). Proof. use isaset_total2. - use isaset_total2. + use impred_isaset. intros t. use setproperty. + intros x. use isasetaprop. use isapropisweq. - intros w. use isasetaprop. use isapropisbinopfun. Qed.