proposition: Lemma um_unitbU k v f : unitb (upd k v f) = false.
proof: Proof. rewrite /unitb /= !umEX /UM.empb /UM.upd. case: (UMC.from f)=>[|f' F] //; case: decP=>// H. suff: k \in supp (ins k v f') by case: (supp _). by rewrite supp_ins inE /= eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)