proposition: Lemma evalUn a p z0 f1 f2 : valid (f1 \+ f2) -> {in dom f1 & dom f2, forall x y, ord x y} -> eval a p (f1 \+ f2) z0 = eval a p f2 (eval a p f1 z0).
proof: Proof. elim/um_indb: f2=>[||k v f2 IH W' P W H]. - by rewrite join_undef valid_undef. - by rewrite dom0 !unitR eval0. rewrite -(joinC f2) joinA in W *; rewrite evalUnPt //; last first. - apply/allP=>x; rewrite domUn inE (validL W). case/orP=>[/H|]; last by apply: P. by apply; rewrite domPtUn inE joinC W' eq_refl. rewrite evalUnPt //; last by apply/allP. rewrite (IH (validL W)) // => k1 k2 D1 D2; apply: H D1 _. by rewrite domPtUn inE joinC W' D2 orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)