proposition: Lemma valid_pval2 (x y : U) : D (pval x) (pval y) = D (pval x) Unit && D (pval y) Unit -> valid (x \+ y) = valid (pval x \+ pval y).
proof: Proof. move=>E; rewrite valid_sep {}E; case W : (valid _)=>//=. move: (validL W) (validR W); rewrite !valid_pval !valid_sep1. by case/andP=>_ -> /andP [_ ->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)