proposition: Lemma oexlt_rcons V R a ks k t (h : natmap V) (z0 : R) : t \in ks -> oexec_lt a (rcons ks k) t h z0 = oexec_lt a ks t h z0.
proof: Proof. by move=>T; rewrite /oexec_lt eqsl_uL_rconsE T. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)