rw [length_cons]
case cons
α : Type u_1
a : α
as : List α
ih : drop as.length as = []
⊢ drop (a :: as).length (a :: as) = []
case cons
α : Type u_1
a : α
as : List α
ih : drop as.length as = []
⊢ drop as.length.succ (a :: as) = []