proposition: Lemma nodup_map_inj A B (f : A -> B) : injective f -> forall l, nodup l -> nodup (map f l).
proof: Proof. intro f_inj. induction l; simpl. auto. intros [a_notin_l l_nodup]. split. 2: fo. intro fa_in_mapfl. destruct (in_map_elim fa_in_mapfl) as [x [x1 x2]]. apply f_inj in x2. subst. contr. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil) CoLoR(FunUtil)