proposition: Lemma validPtPt v1 v2 k : valid (pts k v1 \+ pts k v2 : U) = false.
proof: Proof. by rewrite (validPtUnE v2) validUnEb um_unitbPt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)