proposition: Lemma umallbU p k v f : valid (upd k v f) -> um_allb p (upd k v f) = p (k, v) && um_allb p (free f k).
proof: Proof. rewrite validU=>/andP [W1 W2]; rewrite upd_eta // umallbPtUn //. by rewrite validPtUn W1 validF W2 domF inE eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)