proposition: Lemma oevUn ks (f1 f2 : U) (z0 : R) : valid (f1 \+ f2) -> oeval a ks (f1 \+ f2) z0 = oeval a ks f1 (oeval a ks f2 z0).
proof: Proof. move=>W; elim: ks z0=>[|k ks IH] z0 //=; rewrite findUnL //. case: dom_find=>[E|v E _]; rewrite E IH //. move/In_find/In_dom/(dom_inNL W)/find_none: E=>->; congr oeval; apply/esym. by rewrite oev1 joinC frame joinC -oev1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)