proposition: Lemma uniq_rangeF k f : uniq (range f) -> uniq (range (free f k)).
proof: Proof. case W: (valid f); last first. - by move/negbT/invalidE: W=>->; rewrite free_undef !range_undef. case D : (k \in dom f); last by move/negbT/dom_free: D=>E; rewrite -{1}E. by case: (um_eta D) W=>x [_] E; rewrite {1 2}E; apply: uniq_rangeR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)