proposition: Lemma equiv_of_transfer (T1 T2 : finType) (e1 : rel T1) (e2 : rel T2) (f : T1 -> T2) x y : (forall u v : T1, e1 u v -> equiv_of e2 (f u) (f v)) -> equiv_of e1 x y -> equiv_of e2 (f x) (f y).
proof: Proof. exact: equiv_ofE. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)