proposition: Lemma eqv_clot_nothing' (T : finType) (h : pairs T) : List.Forall (fun p => p.1 = p.2) h -> forall x y, eqv_clot h x y -> x=y.
proof: Proof. intro H. apply eqv_clot_nothing in H. intros x y. rewrite H. apply /eqP. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)