no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : Nodup l
i j : ℕ
hi : i < length l
hj : j < length l
⊢ i = j → nthLe l i hi = nthLe l j hj
simp (config := { contextual := true })