match n with
| 0 =>
  rw [drop_succ_cons]
  rw [drop]
  rw [getElem_eq_get]
  rw [get]
  rw [drop]
| n+1 =>
  rw [drop_succ_cons]
  rw [drop_succ_cons]
  rw [getElem_eq_get]
  rw [get_cons_succ]
  rw [←getElem_eq_get]
  exact ih ..
case cons
α : 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 : n < (a :: as).length
⊢ drop n (a :: as) = (a :: as)[n] :: drop (n + 1) (a :: as)
no goals