proposition: Lemma eqv_clot_mapF (H G : finType) (x : G) (y : H) (l : pairs G) (f : G -> H) : injective f -> y \notin codom f -> eqv_clot (map_pairs f l) (f x) y = false.
proof: Proof. move => inj_f. rewrite /eqv_clot -!lock /=. apply: equiv_of_fn => //. exact: rel_of_pairs_mapE. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)