n : ℕ
α : Type u_1
a : α
l : List α
e : List.length (a :: l) = Nat.succ n
i : ℕ
h : i < n
⊢ List.get (toList (tail { val := a :: l, property := e }))
      { val := i, isLt := (_ : i < List.length (toList (tail { val := a :: l, property := e }))) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }
n : ℕ
α : Type u_1
a : α
l : List α
e : List.length (a :: l) = Nat.succ n
i : ℕ
h : i < n
⊢ get (tail { val := a :: l, property := e }) { val := i, isLt := h } =
    get { val := a :: l, property := e } (Fin.succ { val := i, isLt := h })
simp [get_eq_get]
no goals
n : ℕ
α : Type u_1
a : α
l : List α
e : List.length (a :: l) = Nat.succ n
i : ℕ
h : i < n
⊢ List.get (toList (tail { val := a :: l, property := e }))
      { val := i, isLt := (_ : i < List.length (toList (tail { val := a :: l, property := e }))) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }
rfl