proposition: Lemma oexlt_consec_find V R a t1 t2 (h : natmap V) ks (z0 : R) : uniq ks -> consec ks t1 t2 -> oexec_lt a ks t2 h z0 = if find t1 h is Some e then a (oexec_lt a ks t1 h z0) e else oexec_lt a ks t1 h z0.
proof: Proof. move=>U C; rewrite (oexlt_consec U C). case E : (find t1 h)=>[e|]; first by move/In_find: E=>/(oexleE (consec_mem C)) ->. by rewrite oexleNE // orbC; move/In_findN: E=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)