proposition: Lemma oexle_filter V R a ks p t (h : natmap V) (z0 : R) : (t \notin ks) || (p t) -> oexec_le a (filter p ks) t h z0 = oexec_le a ks t (um_filterk p h) z0.
proof: Proof. by move=>H; rewrite (oexle_umfiltN H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)