proposition: Lemma valid_pval x : valid (pval x) = valid x.
proof: Proof. apply/idP/idP. - by case: X=>pval psub [H1 H2 H3 H4]; apply: H4. move=> Vx; move: (Vx); rewrite -[x]unitL pfjoin //; last by rewrite unitL. by rewrite valid_sep => /andP[]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)