proposition: Lemma InPtUnK k v w f : valid (pts k v \+ f) -> (k, w) \In (pts k v \+ f) <-> v = w.
proof: Proof. move=>W; rewrite InPtUnEN //; split=>[|->]; last by left. by case=>[[->]|[]] //=; rewrite eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)