proposition: Lemma umem_eq_assocs f1 f2 : valid f1 -> valid f2 -> assocs f1 = assocs f2 -> f1 = f2.
proof: Proof. move=>V1 V2 E; apply: umem_eqD V1 V2 _ _. - by rewrite !assocs_dom E. by move=>x /In_assocs; rewrite E=>/In_assocs. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)