proposition: Lemma equiv_of_fn x y : y \notin codom f -> equiv_of e2 (f x) y = false.
proof: Proof. move => yf. apply: contraNF (yf). rewrite equiv_sym/=. move/equiv_of_nn -> => //. exact: codom_f. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)