exact ih ..
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as[n] :: drop (n + 1) as
no goals