proposition: Lemma omap_fresh V V' (h : natmap V) (a : nat * V -> option V') k v : fresh h <= k -> omap a (pts k v \+ h) = (if a (k, v) is Some v' then pts k v' \+ omap a h else omap a h) :> natmap V'.
proof: Proof. case W : (valid h). - by move=>H; rewrite omapPtUn valid_fresh // W. move/negbT/invalidE: W=>->. by case: (a _)=>[w|]; rewrite join_undef omap_undef // join_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)