fact: Definition oex_inv V R (P : R -> Prop) a ks (h : natmap V) (z0 : R) := forall k v, (k, v) \In h -> let z := oexec_lt a ks k h z0 in P z -> P (a z v).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)