proposition: Lemma sep0U x y : valid (x \+ y) -> sep x y -> sep Unit (x \+ y).
proof: Proof. by move=>V S; rewrite sepC ?unitL //; apply: sepU0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)