proposition: Lemma omfresh_dom B h t (f : omap_fun (nat_mapUMC A) (nat_mapUMC B)) : fresh h <= t -> t \notin dom (f h).
proof: Proof. by move=>F; apply/negP=>/omf_subdom/dom_ordfresh; case: ltngtP F. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)