proposition: Lemma eqv_clot_nothing (T : finType) (h : pairs T) : List.Forall (fun p => p.1 = p.2) h -> eqv_clot h =2 eq_op.
proof: Proof. move => /ForallE H x y. rewrite eqv_clotE /= in H *. apply/idP/idP; last by move/eqP->. by apply: equiv_ofE => /= u v /H /= ->. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)