proposition: Lemma oev2_split V R a t1 v (h : natmap V) ks (z0 : R) : t1 \in ks -> (t1, v) \In h -> oevalv a ks h z0 = oevalv a (&=ks `]t1, +oo[) h (a (oexec_lt a ks t1 h z0) v).
proof: Proof. move=>D H; rewrite {1}(eqsl_uoxu ks t1) oev_cat. by rewrite eqsl_xuL D /=; move/In_find: H=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)