proposition: Lemma oexlt_consec_in V R a t1 t2 v (h : natmap V) ks (z0 : R) : uniq ks -> (t1, v) \In h -> consec ks t1 t2 -> oexec_lt a ks t2 h z0 = a (oexec_lt a ks t1 h z0) v.
proof: Proof. move=>U H C; move/slt_memE: (consec_slt C)=>T. by rewrite (oexlt_consec U C) (oexleE T H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)