proposition: Lemma xsep_unitL : left_id xsep_unit xsep_join.
proof: Proof. case=>x qf; apply: xval_inj=>/=. rewrite /xsep_join !unlock /= /xsep_join' /= /xsep_unit unlock /=. rewrite unitL; case: qf=>[|->]; last by rewrite tpcmE. by case/andP=>W E; rewrite sepC ?unitL // W E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)