proposition: Lemma oexle_cons_notin V R a ks k t (h : natmap V) (z0 : R) : k \notin dom h -> t != k -> oexec_le a (k :: ks) t h z0 = oexec_le a ks t h z0.
proof: Proof. move=>H Ntk; rewrite /oexec_le [in LHS]oevFK [in RHS]oevFK. by rewrite eqsl_uL_consE (negbTE Ntk) /= (negbTE H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)