proposition: Lemma sepU0 x y : valid (x \+ y) -> sep x y -> sep (x \+ y) Unit.
proof: Proof. move=>V S1. move/(sepx0 V): S1 (S1)=>S1 S2. rewrite -[x]unitR in V S2. by rewrite sepC ?(sepAxx V S1 S2) // joinAC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)