proposition: Lemma eq_in_oevK a ks1 ks2 f z0 : [seq k <- ks1 | k \in dom f] = [seq k <- ks2 | k \in dom f] -> oeval a ks1 f z0 = oeval a ks2 f z0.
proof: Proof. suff oevFK ks : oeval a ks f z0 = oeval a [seq k <- ks | k \in dom f] f z0. - by move=>E; rewrite oevFK E -oevFK. by elim: ks z0=>[|k' ks IH] z0 //=; case: dom_find=>[->|v /= -> _]; rewrite IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)