proposition: Lemma pfV2_phant U V D (f : @morphism U V D) of phantom (_ -> _) f : forall x y, valid (x \+ y) -> D x y -> valid (f x \+ f y).
proof: Proof. by move=>x y; apply: pfV2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)