proposition: Lemma xsep_unitbP x : reflect (x = Unit) (xsep_unitb x).
proof: Proof. rewrite /Unit /= /xsep_unit unlock /xsep_unitb; case: x=>x H /=. case: unitbP=>X; constructor; last by case=>/X. by rewrite X in H *; rewrite (pf_irr H xsep_unitP). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)