proposition: Lemma lift_equiv (T1 T2 : finType) (E1 : rel T1) (E2 : rel T2) h : bijective h -> (forall x y, E1 x y = E2 (h x) (h y)) -> (forall x y, equiv_of E1 x y = equiv_of E2 (h x) (h y)).
proof: Proof. move=> [hinv] hK hinvK hE x y. rewrite /equiv_of. apply/idP/idP. - by apply: homo_connect => {x y} x y /=; rewrite !hE. - rewrite -{2}(hK x) -{2}(hK y). by apply: homo_connect => {x y} x y /=; rewrite !hE !hinvK. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)