proposition: Lemma kernelP A (B : eqType) (f : A -> B) x y : reflect (kernel f x y) (kernelb f x y).
proof: Proof. exact: (iffP eqP). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)