proposition: Lemma eqv_clot_eq (T: finType) (h k: pairs T): List.Forall (fun p => eqv_clot k p.1 p.2) h -> List.Forall (fun p => eqv_clot h p.1 p.2) k -> eqv_clot h =2 eqv_clot k.
proof: Proof. move=> A B x y. by apply/idP/idP; apply eqv_clot_subrel. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)