proposition: Lemma oev0 a ks z0 : oeval a ks Unit z0 = z0.
proof: Proof. by elim: ks=>[|k ks IH] //=; rewrite find0E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)