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