proposition: Lemma oex_xx 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_le a ks t2 h z0).
proof: Proof. move=>U T IH P0; rewrite /oexec_le (eqsl_uxox 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_ox: (K)=>// [Ks 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 eqsl_xxL T2K Ks /= => 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)