proposition: Lemma eq_in_oevF a ks f1 f2 z0 : (forall k v, k \in ks -> (k, v) \In f1 <-> (k, v) \In f2) -> oeval a ks f1 z0 = oeval a ks f2 z0.
proof: Proof. elim: ks z0=>[|k ks IH] z0 //= H. case E1: (find k f1)=>[v1|]. - move/In_find: E1; rewrite H ?(inE,eq_refl) // => /In_find ->. by apply: IH=>k' v' D; apply: H; rewrite inE D orbT. case E2: (find k f2)=>[v2|]. - by move/In_find: E2; rewrite -H ?(inE,eq_refl) // => /In_find; rewrite E1. by apply: IH=>k' v' D; apply: H; rewrite inE D orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)