proposition: Lemma umcompPtf f k v : um_comp (pts k v) f = if C2 k then omap (fun x => if x.2 == k then Some v else None) f else if valid f then Unit else undef.
proof: Proof. elim/um_indf: f=>[||x w f IH W P]. - rewrite umcomp_fundef omap_undef. by case: ifP=>//; rewrite valid_undef. - rewrite umcompf0 omap0. by case: ifP=>//; rewrite valid_unit. rewrite umcompfUn // umcompfPt (validPtUn_cond W) omapPtUn. rewrite W findPt2 andbC. case C: (C2 k) IH=>/= IH; last by rewrite IH (validR W) unitL. by case: eqP=>_; rewrite IH // unitL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)