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