apply nodup_of_get_inj
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ Nodup (List.map f l)
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ ∀ (i j : Nat) (x : i < length (List.map f l)) (x_1 : j < length (List.map f l)),
    (List.map f l)[i] = (List.map f l)[j] → i = j