proposition: Lemma oev_dom0 a ks f z0 : dom f =i [::] -> oeval a ks f z0 = z0.
proof: Proof. case W : (valid f); first by move/(dom0E W)=>->; apply: oev0. by move/negbT/invalidE: W=>-> _; apply: oev_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)