proposition: Lemma kerX (U : pcm) (V : tpcm) (D : rel U) (f : @morphism U V D) x y : 'ker f x y = [&& D x y, unitb (f x) & unitb (f y)].
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)