proposition: Lemma dom_omfreshT B h x t (f : omap_fun (nat_mapUMC A) (nat_mapUMC B)) : fresh h <= t -> x \in dom (f h) -> x != t.
proof: Proof. by move=>H1 /dom_omfresh H2; case: ltngtP (leq_trans H2 H1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)