proposition: Lemma eqv_clotE (T : finType) (l : pairs T) x y : eqv_clot l x y = equiv_of (rel_of_pairs l) x y.
proof: Proof. by rewrite /eqv_clot -lock. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)