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