proposition: Lemma oex3_split V R a t1 t2 t3 v1 v2 (h : natmap V) ks (z0 : R) : t1 <[ks] t2 -> (t1, v1) \In h -> t2 <[ks] t3 -> (t2, v2) \In h -> oexec_lt a ks t3 h z0 = oevalv a (&=ks `]t2, t3[) h (a (oevalv a (&=ks `]t1, t2[) h (a (oexec_lt a ks t1 h z0) v1)) v2).
proof: Proof. move=>T1 H1 T2 H2. by rewrite (oex2_split T2 H2) (oex2_split T1 H1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)