proposition: Lemma oevFK a ks f z0 : oeval a ks f z0 = oeval a [seq k <- ks | k \in dom f] f z0.
proof: Proof. 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)