proposition: Lemma oexlt_consec_fst V R a t (h : natmap V) k ks (z0 : R) : uniq (k::ks) -> k \notin dom h -> t \in k::ks -> consec (k::ks) k t -> oexec_lt a (k::ks) t h z0 = z0.
proof: Proof. move=>U K T C; case/(consecP_split _ U T): C=>xs1 [xs2] X. case: xs1 X U {T}=>[|x xs1]; last first. - by case=>->-> /=; rewrite mem_cat inE eqxx !orbT. case=>->{ks}; rewrite /= inE negb_or -andbA; case/and4P=>U1 U2 U3 U4. rewrite oexlt_cons_notin ?inE 1?negb_or ?(eq_sym t) ?U1 ?U2 //. by rewrite oexlt_cons_same. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)