proposition: Lemma oexlt_cons V R a ks k t v (h : natmap V) (z0 : R) : (k, v) \In h -> t != k -> oexec_lt a (k :: ks) t h z0 = oexec_lt a ks t h (a z0 v).
proof: Proof. move=>H Ntk; rewrite /oexec_lt eqsl_uL_consE (negbTE Ntk) /=. by 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)