proposition: Lemma oevF a ks f z0 k : k \notin ks -> oeval a ks f z0 = oeval a ks (free f k) z0.
proof: Proof. move=>H; apply: eq_in_oevF=>k' v' D; rewrite InF /= validF. by case: eqP H D=>[-> /negbTE -> //|???]; split; [move=>H; case: (H) | case]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)