proposition: Lemma updU k1 k2 v1 v2 f : upd k1 v1 (upd k2 v2 f) = if k1 == k2 then upd k1 v1 f else upd k2 v2 (upd k1 v1 f).
proof: Proof. rewrite !umEX /UM.upd. case: (UMC.from f)=>[|f' H']; case: ifP=>// E; case: decP=>H1; case: decP=>H2 //; rewrite !umEX. - by rewrite ins_ins E. - by rewrite (eqP E) in H2 *. by rewrite ins_ins E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)