proposition: Lemma omf_subfresh t e h : fresh h <= t -> {subset dom (f h) <= dom (f (t \-> e \+ h))}.
proof: Proof. move=>N x H; rewrite omf_fresh //; case: (map_fun _ _)=>[a|//]. by rewrite domPtUn inE H orbT valid_fresh ?(dom_valid H, fresh_omfT). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)