proposition: Lemma oexF_uu V R X (f : R -> X) a ks (h : natmap V) (z0 : R) : uniq ks -> {in ks, oexF_inv f a ks h z0} -> f (oevalv a ks h z0) = f z0.
proof: Proof. move=>U H; pose P := fun x => f x = f z0. by apply: (oex_uu 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)