proposition: Lemma xsep_undef_join x : xsep_undef \+ x = xsep_undef.
proof: Proof. apply: xval_inj; rewrite /= pcm_joinE /xsep_undef /=. by rewrite /xsep_join !unlock /= /xsep_join' !tpcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)