proposition: Lemma domUE k e f : k \in dom f -> dom (upd k e f) = dom f.
proof: Proof. move=>H; apply/domE=>x; rewrite domU inE (dom_cond H) /=. by case: eqP=>// ->; rewrite H (dom_valid H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)