proposition: Lemma valid_sep1 (x : U) : valid x = valid (pval x) && D (pval x) Unit.
proof: Proof. by rewrite -[x]unitR valid_sep pfunit !unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)