proposition: Lemma oex_uu V R (P : R -> Prop) a ks (h : natmap V) (z0 : R) : uniq ks -> {in ks, oex_inv P a ks h z0} -> P z0 -> P (oevalv a ks h z0).
proof: Proof. move=>U IH P0; apply: oev_indX=>// k ks1 ks2 v _ Kh Eh ->. have K : k \in ks by rewrite Eh mem_cat inE eqxx orbT. have Nk : k \notin ks1. - move: U. by rewrite Eh cat_uniq /= negb_or -andbA; case/and5P. suff -> : ks1 = &=ks `]-oo, k[ by apply: IH. move: Eh; rewrite {1}(eqsl_uxou ks k) eqsl_uxR K -cats1 -catA /= => Eh. by rewrite (cat_cancel _ _ Eh) //=; apply: eqsliceRO_notin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)