proposition: Lemma oexF_xo V R X (f : R -> X) a ks (h : natmap V) t1 t2 (z0 : R) : uniq ks -> t1 <=[ks] t2 -> {in &=ks `[t1, t2], oexF_inv f a ks h z0} -> f (oexec_le a ks t2 h z0) = f (oexec_lt a ks t1 h z0).
proof: Proof. move=>U T H; pose P := fun x => f x = f (oexec_lt a ks t1 h z0). by apply: (oex_xo P) T _ _=>// 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)