proposition: Lemma homoW_in : {in D & D', {homo f : x y / aR' x y >-> rR' x y}} -> {in D & D', {homo f : x y / aR x y >-> rR x y}}.
proof: Proof. by move=> mf x y xD yD /[!aRE]/orP[/eqP->|/mf]; rewrite rRE ?eqxx// orbC => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)