proposition: Lemma evalFU k v z0 f : valid (upd k v f) -> eval a p (upd k v f) z0 = if p (k, v) then a Unit k v \+ eval a p (free f k) z0 else eval a p (free f k) z0.
proof: Proof. move=>W; move: (W); rewrite validU =>/andP [C1 _]. have /um_eta2 E : find k (upd k v f) = Some v. - by rewrite findU eq_refl -(validU k v) W. by rewrite E evalFPtUn -?E // freeU eq_refl C1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)