proposition: Lemma xvalid_pval x : valid (xval x) -> valid x.
proof: Proof. rewrite {2}/valid /= /xsep_valid /= unlock. by case: x=>x /= [/andP [->->]|] // ->; rewrite tpcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)