α : Type u_1
a : α
l x✝ : List α
n : Nat
h : n + 1 < length (a :: l)
⊢ get (List.append l x✝) { val := Nat.add n 0, isLt := (_ : succ (Nat.add n 0) ≤ length (List.append l x✝)) } =
    get l { val := Nat.add n 0, isLt := (_ : succ (Nat.add n 0) ≤ length l) }
α : Type u_1
a : α
l x✝ : List α
n : Nat
h : n + 1 < length (a :: l)
⊢ get (a :: l ++ x✝) { val := n + 1, isLt := (_ : n + 1 < length (a :: l ++ x✝)) } =
    get (a :: l) { val := n + 1, isLt := h }
simp only [get, cons_append]
no goals
α : Type u_1
a : α
l x✝ : List α
n : Nat
h : n + 1 < length (a :: l)
⊢ get (List.append l x✝) { val := Nat.add n 0, isLt := (_ : succ (Nat.add n 0) ≤ length (List.append l x✝)) } =
    get l { val := Nat.add n 0, isLt := (_ : succ (Nat.add n 0) ≤ length l) }
apply get_append