proposition: Lemma xsep_joinP x y : xsepP (xsep_join' x y).
proof: Proof. rewrite /xsepP /xsep_join'; case: ifP; last by right. by case/andP=>W /(sepU0 W) ->; rewrite W; left. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)