proposition: Lemma InPtUn x k v f : x \In pts k v \+ f -> [/\ [&& C k, valid f & k \notin dom f] & (x = (k, v) /\ C k \/ x \In f /\ x.1 != k)].
proof: Proof. move=>H; have W w : valid (pts k w \+ f). - by rewrite (validPtUnE v); apply: dom_valid (In_dom H). rewrite (validPtUnI (W v)); split=>//; move/(InPtUnEN _ (W v)): H (W v). by case=>[-> /validPtUn_cond|]; [left | right]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)