proposition: Lemma oexF_ux V R X (f : R -> X) a ks (h : natmap V) t (z0 : R) : uniq ks -> {in &=ks `]t, +oo[, oexF_inv f a ks h z0} -> f (oevalv a ks h z0) = f (oexec_le a ks t h z0).
proof: Proof. move=>U H; pose P := fun x => f x = f (oexec_le a ks t h z0). by apply: (oex_ux P)=>// x S v K E; rewrite /P -E; apply: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)