proposition: Lemma idsubpcm_valid_psub (x y : U) : valid (x \+ y) -> valid (x \+ y) && sepT x y.
proof: Proof. by rewrite andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)