proposition: Lemma pfV2 x y : valid (x \+ y) -> D x y -> valid (f x \+ f y).
proof: Proof. by move=>H S; case: (pfjoinV H S). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)