proposition: Lemma oexle_umfilt V R a ks p t (h : natmap V) (z0 : R) : oexec_le a ks t (um_filterk p h) z0 = oevalv a (filter p (&=ks `]-oo, t])) h z0.
proof: Proof. by rewrite /oexec_le oev_filter. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)