proposition: Lemma oexleE V R a t v (h : natmap V) ks (z0 : R) : t \in ks -> (t, v) \In h -> oexec_le a ks t h z0 = a (oexec_lt a ks t h z0) v.
proof: Proof. by move=>K H; rewrite /oexec_le/oexec_lt eqsl_uxR K (oev_rconsP _ _ _ H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)