proposition: Lemma oex_ox V R (P : R -> Prop) a ks (h : natmap V) t1 t2 (z0 : R) : uniq ks -> t1 <[ks] t2 -> {in &=ks `]t1, t2[, oex_inv P a ks h z0} -> P (oexec_le a ks t1 h z0) -> P (oexec_lt a ks t2 h z0).
proof: Proof. move=>U T IH P0; rewrite /oexec_lt (eqsl_uxoo T) oev_cat. apply: oev_indX=>// k ks1 ks2 v _ Kh Eh ->; rewrite -oev_cat. have K : k \in &=ks `]t1, t2[ by rewrite Eh mem_cat inE eqxx orbT. have Nk : k \notin ks1. - move/(eqslice_uniq `]t1, t2[): U. by rewrite Eh cat_uniq /= negb_or -andbA; case/and5P. case/mem_oo: (K)=>// [_ T1K T2K]. suff {IH U K}-> : ks1 = &=ks `]t1, k[ by rewrite -eqsl_uxoo //; apply: IH. move: Eh; rewrite (eqslice_split (b:=true) (x:=k)) /=; last by apply/andP; rewrite !lteBSide /= leEnat; split=>//=; apply: ltnW. rewrite eqsl_xoL T2K /= => Eh; rewrite (cat_cancel _ _ Eh) //. by 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)