proposition: Lemma oexlt_consec V R a ks t1 t2 (h : natmap V) (z0 : R) : uniq ks -> consec ks t1 t2 -> oexec_lt a ks t2 h z0 = oexec_le a ks t1 h z0.
proof: Proof. move=>U C; apply: (oexF_ox id)=>//; first by apply: consec_slt. by move=>x; rewrite consec_oo. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)