proposition: Lemma eval_eq A R a (h : natmap A) t v (z0 : R) : (t, v) \In h -> eval a [pts k _ | k == t] h z0 = a z0 t v.
proof: Proof. move=>H; rewrite eval_umfilt; have N : t != 0 by move/In_dom/dom_cond: H. suff -> : um_filter [pts k _ | k == t] h = t \-> v by rewrite evalPt /= N. apply/umem_eq=>[||[k w]]; first by rewrite valid_umfilt; case: H. - by rewrite validPt. rewrite In_umfilt; split; last by move/InPt =>[[->->]]. by move=>[/eqP -> H1]; rewrite (In_fun H H1); apply: In_condPt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)