proposition: Lemma upd_inj k v1 v2 f : valid f -> C k -> upd k v1 f = upd k v2 f -> v1 = v2.
proof: Proof. rewrite !pcmE /= !umEX /UM.valid /UM.upd. case: (UMC.from f)=>[|f' F] // _; case: decP=>// H _ E. have: fnd k (ins k v1 f') = fnd k (ins k v2 f') by rewrite E. by rewrite !fnd_ins eq_refl; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)