proposition: Lemma omapU k (v : V) (f : U) : omap a (upd k v f) = if C k then if a (k, v) is Some v' then upd k v' (omap a f) else free (omap a f) k : U' else undef.
proof: Proof. case: ifP=>// W; last first. - have: ~~ valid (upd k v f) by rewrite validU W. by move/invalidE=>->; apply omap_undef. case H: (valid f); last first. - move: H; move/negbT/invalidE=>->; rewrite upd_undef omap_undef free_undef. by case: (a (k, v)) =>// a0; rewrite upd_undef. rewrite upd_eta // omapPtUn validPtUn W validF H domF inE eq_refl /=. case E: (a (k, v))=>[xa|]; last by rewrite omapF. by rewrite upd_eta omapF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)