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