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

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

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