proposition: Lemma kernel_eqv_clot {A: finType} {B:eqType} (l: pairs A) (f: A -> B): List.Forall (fun p => f p.1 = f p.2) l -> (forall x y, f x = f y -> eqv_clot l x y) -> (forall x y, reflect (kernel f x y) (eqv_clot l x y)).
proof: Proof. move => /ForallE H1 H2 x y. apply: (iffP idP); last exact: H2. move => E. apply/kernelP. suff: subrel (eqv_clot l) (EquivRelPack (kernel_equivalence f)) by apply. rewrite /eqv_clot -lock. apply equiv_of_sub'. by move => {E x y} x y /= /H1/eqP. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)