proposition: Lemma xsep_joinC : commutative xsep_join.
proof: Proof. case=>x Hx [y Hy]; apply: xval_inj. rewrite /= /xsep_join !unlock /= /xsep_join' /=. by rewrite joinC; case W: (valid _)=>//=; rewrite -sepC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)