rw [drop]
α : 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
⊢ drop 0 (a :: as) = (a :: as)[0] :: 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 :: as)[0] :: drop 0 as