Theorem: LoVe.drop_nil (LoVe/Labs/Lab4Solution.lean)

State before:
α : Type
⊢ drop 0 [] = []
Tactic:
rfl
State after:
no goals

State before:
α : Type
n✝ : ℕ
⊢ drop (n✝ + 1) [] = []
Tactic:
rfl
State after:
no goals