proposition: Lemma InPtUnEN k v x f : valid (pts k v \+ f) -> x \In (pts k v \+ f) <-> x = (k, v) \/ x \In f /\ x.1 != k.
proof: Proof. move=>W; rewrite InPtUnE //; split; last by case; [left|case; right]. case=>[->|H]; first by left. right; split=>//; move/In_dom: H=>H. case: validUn W=>//; rewrite validPt=>W W' /(_ k). rewrite domPt inE W eq_refl /= => /(_ (erefl _)). by case: eqP H=>// ->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)