proposition: Lemma uniq_assocs K C (V : eqType) (U : @union_map_class K C V) (f : U) : uniq (assocs f).
proof: Proof. rewrite !umEX /UM.assocs /=; case: (UMC.from f)=>[|[s H _]] //=. by move/(sorted_uniq (@trans K) (@irr K)): H; apply: map_uniq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)