proposition: Lemma assocsPtUn f k v : valid (pts k v \+ f) -> all (ord k) (dom f) -> assocs (pts k v \+ f) = (k, v) :: (assocs f).
proof: Proof. rewrite !pcmE /= !umEX /UM.assocs/UM.union/UM.pts/UM.dom/supp /=. case: decP=>// H1; case: (UMC.from f)=>//= g H2. rewrite /disj /= andbT; case: ifP=>//= D _ H3. rewrite (fcat_inss _ (@nil K V) D) fcat0s. case: g H2 D H3=>//= g P H2 D H3. by apply: last_ins'; rewrite path_min_sorted //. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)