proposition: Lemma oev_ind2 {P : R1 -> R2 -> Prop} (f : U) ks a1 a2 z1 z2 : P z1 z2 -> (forall k v z1 z2, (k, v) \In f -> k \in ks -> P z1 z2 -> P (a1 z1 k v) (a2 z2 k v)) -> P (oeval a1 ks f z1) (oeval a2 ks f z2).
proof: Proof. elim: ks a1 a2 z1 z2=>[|k ks IH] a1 a2 z1 z2 Z H //=. apply: IH; last first. - by move=>k' v' z1' z2' H' K'; apply: H=>//; rewrite inE K' orbT. case H' : (find k f)=>[b|] //; move/In_find: H'=>H'. 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)