proposition: Lemma xsep_valid_undef : ~~ valid xsep_undef.
proof: Proof. by rewrite pcmE /= /xsep_valid /= /xsep_undef !unlock /= tpcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)