proposition: Lemma xsepP_st (x : xsepPCM D) : x = undef \/ valid x.
proof: Proof. set X := xsepSubPCM_st D; rewrite (valid_sep1 X). case: x=>x [H|H]; [right=>//|left]; subst x. by apply: (pval_inj (X:=X)); rewrite /= xval_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)