proposition: Lemma eqv_clot_subrel (T: finType) (h k: pairs T): List.Forall (fun p => eqv_clot k p.1 p.2) h -> subrel (eqv_clot h) (eqv_clot k).
proof: Proof. rewrite ForallE=>H x y. rewrite eqv_clotE. apply equiv_of_sub'=> u v. exact (H (u,v)). Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)