proposition: Lemma oev1 ks f z0 : oeval a ks f z0 = oeval a ks f Unit \+ z0.
proof: Proof. apply: (oev_ind2 (P:=fun r1 r2 => r1 = r2 \+ z0)); first by rewrite unitL. by move=>k v z1 z2 H1 H2 ->; apply: frame. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)