proposition: Lemma oev_oexle_last V R a k ks (h : natmap V) (z0 : R) : uniq (k::ks) -> oevalv a (k::ks) h z0 = oexec_le a (k::ks) (last k ks) h z0.
proof: Proof. case/andP=>U1 U2; rewrite /oexec_le eqsl_uL_consE. case: eqP=>/= [/last_nochange|/eqP/last_change H]. - by rewrite (negbTE U1)=>/eqP->. by congr oeval; apply/eqsl_lastR_uniq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)