proposition: Lemma oexle_rcons_notin_in V R a ks k t v (h : natmap V) (z0 : R) : (k, v) \In h -> t \notin ks -> oexec_le a (rcons ks k) t h z0 = a (oexec_le a ks t h z0) v.
proof: Proof. move=>H T; rewrite oexle_rcons_notin // oev_rconsE. by move/In_find: (H)=>->; rewrite oexleNE ?T // /oexec_lt eqsl_uL_notinE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)