proposition: Lemma assocsUnPt f k v : valid (f \+ pts k v) -> all (ord^~ k) (dom f) -> assocs (f \+ pts k v) = rcons (assocs f) (k, v).
proof: Proof. rewrite !pcmE /= !umEX /UM.assocs/UM.union/UM.pts/UM.dom/supp /=. case: (UMC.from f)=>//=; case: decP=>//= H1 g H2; case: ifP=>//= _ _. by case: allP=>//; case: g H2=>// s1 H2 H3 H4 _; apply: first_ins' H4. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)