proposition: Lemma InU x k v f : x \In upd k v f <-> [/\ valid (upd k v f) & if x.1 == k then x.2 = v else x \In f].
proof: Proof. case: x=>x1 v1; split; last first. - case=>W /= H; split=>//=; exists (free (upd k v f) x1); apply: um_eta2. move: (W); rewrite validU=>/andP [C' W']; rewrite findU C' W' /=. by case: eqP H=>[_ ->|_ /In_find]. move=>H; move: (In_dom H)=>/= D; move: (dom_valid D) (dom_valid D)=>W. rewrite {1}validU=>/andP [C' W']; split=>//. move: (D); rewrite domU inE C' /= W'; case: H=>/= _ [z E]. case: ifP D E=>[/eqP -> D E _|N _ E D]. - have: find k (upd k v f) = Some v by rewrite findU eq_refl C' W'. by rewrite E findPtUn -?E //; case=>->. have: find x1 (pts x1 v1 \+ z) = Some v1 by rewrite findPtUn // -E. by rewrite -E findU N C'=>/In_find. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)