proposition: Lemma xval_morphP : morph_axiom (sepT_seprel xsepPCM) xval.
proof: Proof. split=>[|x y]; first by rewrite pcmE /= /xsep_unit /= unlock. rewrite {1}/valid /= /xsep_valid /= pcm_joinE /= /xsep_join !unlock /xsep_join' /=; by case: ifP; rewrite ?tpcmE //; case/andP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)