proposition: Lemma updF k1 k2 v f : upd k1 v (free f k2) = if k1 == k2 then upd k1 v f else free (upd k1 v f) k2.
proof: Proof. rewrite !umEX /UM.dom /UM.upd /UM.free. case: (UMC.from f)=>[|f' F] //; case: ifP=>// H1; by case: decP=>H2 //; rewrite !umEX ins_rem H1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)