proposition: Lemma oev_ind {P : R -> Prop} f ks a z0 : P z0 -> (forall k v z0, (k, v) \In f -> k \in ks -> 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. - by move=>k' v' z' X D; apply: H=>//; rewrite inE D orbT. case E: (find k f)=>[b|] //; move/In_find: E=>E. by apply: H=>//; rewrite inE eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)