proposition: Lemma oexlt_cons_same V R a ks k (h : natmap V) (z0 : R) : oexec_lt a (k :: ks) k h z0 = z0.
proof: Proof. by rewrite /oexec_lt eqsl_uL_consL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)