no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
H : Nodup l
i : Fin (length l)
⊢ get l { val := indexOf (get l i) l, isLt := (_ : indexOf (get l i) l < length l) } = get l i
simp