proposition: Lemma pfV (U : pcm) V (D : rel U) (f : @morphism U V D) x : valid x -> D x Unit -> valid (f x).
proof: Proof. by rewrite -{1 3}[x]unitR=>W S; rewrite pfjoin //; apply: pfV2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)