proposition: Lemma eqv_clot_map' (aT rT : finType) (f : aT -> rT) (l : pairs aT) x y : eqv_clot l x y -> eqv_clot (map_pairs f l) (f x) (f y).
proof: Proof. rewrite eqv_clotE /=. apply: equiv_ofE => {x y} x y H. apply: eqv_clot_pair. by apply/mapP; exists (x,y). Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)