proposition: Lemma oexlt_umfiltN V R a ks p t (h : natmap V) (z0 : R) : (t \notin ks) || (p t) -> oexec_lt a ks t (um_filterk p h) z0 = oexec_lt a (filter p ks) t h z0.
proof: Proof. move=>H; rewrite /oexec_lt oev_umfilt eqsl_filterL //=. apply: eq_in_oevK; rewrite -!filter_predI; apply: eq_in_filter=>k Ks /=. by case D : (k \in dom h)=>//=; case/In_domX: D=>v /In_find ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)