α : Type u_1
a : α
l x✝ : List α
n : Nat
h₁ : length (a :: l) ≤ n + 1
⊢ get? (a :: (l ++ x✝)) (n + 1) = get? x✝ (n + 1 - length (a :: l))
α : Type u_1
a : α
l x✝ : List α
n : Nat
h₁ : length (a :: l) ≤ n + 1
⊢ get? (a :: l ++ x✝) (n + 1) = get? x✝ (n + 1 - length (a :: l))
rw [cons_append]
no goals
α : Type u_1
a : α
l x✝ : List α
n : Nat
h₁ : length (a :: l) ≤ n + 1
⊢ get? (a :: (l ++ x✝)) (n + 1) = get? x✝ (n + 1 - length (a :: l))
simp [get?_append_right (Nat.lt_succ.1 h₁)]