rw [get]
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as).get ⟨0, hn⟩ :: drop 0 as
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = a :: drop 0 as