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