proposition: Lemma oexle_cat V R a ks1 ks2 t (h : natmap V) (z0 : R) : t \notin ks1 -> oexec_le a (ks1 ++ ks2) t h z0 = if t \in ks1 then oexec_le a ks1 t h z0 else oexec_le a ks2 t h (oexec_le a ks1 t h z0).
proof: Proof. move=>T; rewrite /oexec_le eqsl_uL_catE (negbTE T). by rewrite oev_cat (eqsl_uL_notinE (s:=ks1)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)