proposition: Lemma oexle_cons V R a ks k t v (h : natmap V) (z0 : R) : (k, v) \In h -> oexec_le a (k :: ks) t h z0 = if t == k then a z0 v else oexec_le a ks t h (a z0 v).
proof: Proof. move=>H; rewrite /oexec_le eqsl_uL_consE. by case: eqP=>/=; 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)