proposition: Lemma fresh_omap_some V1 V2 (f : nat * V1 -> option V2) (h : natmap V1) : (forall x, x \In h -> oapp predT false (f x)) -> fresh (omap f h) = fresh h.
proof: Proof. by move=>H; rewrite /fresh lastkey_omap_some. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)