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