proposition: Lemma eqv_clot_map_eq (H G : finType) (x y : H) (l : pairs G) (f : G -> H) : x \notin codom f -> eqv_clot (map_pairs f l) x y = (x == y).
proof: Proof. move => cd_x. apply/idP/eqP; last by move => ->. rewrite /eqv_clot -!lock /=. apply: equiv_of_nn cd_x => //. exact: rel_of_pairs_mapE. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)