proposition: Lemma xsep_valid_unit : xsep_valid xsep_unit.
proof: Proof. by rewrite /xsep_valid/xsep_unit /= !unlock valid_unit sep00. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)