proposition: Lemma pts_undef2 k v1 v2 : pts k v1 \+ pts k v2 = undef :> U.
proof: Proof. apply/invalidE; rewrite validPtUn validPt domPt !negb_and negb_or eq_refl. by case: (C k). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)