proposition: Lemma oev_indX {P : R -> Prop} f ks a z0 : P z0 -> (forall k ks1 ks2 v z0', (k, v) \In f -> ks = ks1 ++ k :: ks2 -> z0' = oeval a ks1 f z0 -> P z0' -> P (a z0' k v)) -> P (oeval a ks f z0).
proof: Proof. elim: ks z0=>[|k ks IH] z0 //= Z H; apply: IH; last first. - move=>k' ks1 ks2 v' z' X D E. by apply: (H k' (k::ks1) ks2 v' z' X _ _)=>//; rewrite D. case E: (find k f)=>[b|] //; move/In_find: E=>E. by apply: (H k [::] _ b z0). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)