proposition: Lemma uniq_dom f : uniq (dom f).
proof: Proof. apply: sorted_uniq (sorted_dom f); by [apply: ordtype.trans | apply: ordtype.irr]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)