α : Type u_1
b : α
l : List α
a : α
⊢ get? (b :: (l ++ [a])) (succ (length l)) = some a
α : Type u_1
b : α
l : List α
a : α
⊢ get? (b :: l ++ [a]) (length (b :: l)) = some a
rw [cons_append, length_cons]
no goals
α : Type u_1
b : α
l : List α
a : α
⊢ get? (b :: (l ++ [a])) (succ (length l)) = some a
simp only [get?, get?_concat_length]