proposition: Lemma eval_leF A R X a (f : R -> X) (h : natmap A) t1 t2 (z0 : R) : t1 <= t2 -> (forall k v z0, (k, v) \In h -> t1 < k <= t2 -> f (a z0 k v) = f z0) -> f (eval a (le t1) h z0) = f (eval a (le t2) h z0).
proof: Proof. move=>T H. apply: (eval_le_ind (P := fun x => f (eval a (le t1) h z0) = f x)) T _ _=>//. by move=>k v z1 H1 /H ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)