proposition: Lemma oexleNE V R a t (h : natmap V) ks (z0 : R) : (t \notin ks) || (t \notin dom h) -> oexec_le a ks t h z0 = oexec_lt a ks t h z0.
proof: Proof. rewrite /oexec_le/oexec_lt; case K: (t \in ks)=>/= H; last first. - rewrite (eqsl_uoxx (t1:=t) (t2:=t)); last by exact: sle_refl. by rewrite eqsl_kk1 /= K cats0. rewrite [LHS]oevFK [RHS]oevFK; congr oeval. by rewrite eqsl_uxR K filter_rcons (negbTE H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)