proposition: Lemma omf_fresh t e h : fresh h <= t -> f (t \-> e \+ h) = if map_fun f (t, e) is Some v then t \-> v \+ f h else f h.
proof: Proof. by case: f=>s [m H] /= N; rewrite !H omap_fresh. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)