proposition: Lemma equiv_of_nn x y : x \notin codom f -> equiv_of e2 x y -> x = y.
proof: Proof. move => xf. case/connectP => p. elim: p x xf => /=; auto. move => z p _ x xf /andP[E _] _. apply: contraNeq xf => _. case/orP : E => /eq2E [?] [?] [? ?]; subst; exact: codom_f. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)