rfl
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ l { val := (castSucc k).val, isLt := ?hc } = l k

case hc
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ (castSucc k).val < n
no goals