induction l with
| nil => exact .nil
| cons a l IH =>
  refine .cons ?_ (IH fun i j hi hj hl => ?_)
  . intro _ hmem heq; cases heq
    have ⟨⟨i,hi⟩,hl⟩ := List.mem_iff_get.mp hmem
    have : i+1 = 0 :=
      h (i+1) 0 (Nat.succ_lt_succ hi) l.length.zero_lt_succ hl
    cases this
  . apply Nat.succ.inj
    exact h (i+1) (j+1) (Nat.succ_lt_succ hi) (Nat.succ_lt_succ hj) hl
α : Type u
β : Type v
l : List α
h : ∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j
⊢ Nodup l
no goals