proposition: Lemma eqv_clot_tl (T: finType) (x y: T) z (l: pairs T): eqv_clot l x y -> eqv_clot (z::l) x y.
proof: Proof. exact: eqv_clot_subset. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)