proposition: Lemma oexle_rcons_same V R a ks k (h : natmap V) (z0 : R) : k \notin ks -> oexec_le a (rcons ks k) k h z0 = oevalv a (rcons ks k) h z0.
proof: Proof. exact: oexle_rcons_notin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)