proposition: Lemma upd_condN k v f : ~~ C k -> upd k v f = undef.
proof: Proof. rewrite /undef /= !umEX /UM.upd. case: (UMC.from f)=>[|f' H']=>//. by case: decP=>//= ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)