proposition: Lemma uniq_map_2 : uniq E -> uniq (map f1 f2 E).
proof: Proof. clear. intros J. induction E as [ | a E']; simpl_asnlist in *. apply uniq_nil. inversion J; subst. simpl_asnlist. apply uniq_push. auto. rewrite dom_map. trivial. inversion J; subst. simpl_asnlist. apply uniq_alt. auto. Qed.
imports: Coq.FSets.FSets Coq.Lists.List Coq.Logic.Decidable Metalib.CoqFSetDecide Metalib.CoqListFacts Metalib.LibTactics Metalib.MetatheoryAtom Metalib.LibTactics