proposition: Lemma inj_homo_in : {in D & D', injective f} -> {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. move=> fI mf x y xD yD /[!(aR'E, rR'E)] /andP[neq_xy xy]. by rewrite mf ?andbT//; apply: contra_neq neq_xy; apply: fI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)