no goals
ι : Type ?u.216866
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n m : ℕ
⊢ drop n (drop m []) = drop (n + m) []
simp
no goals
ι : Type ?u.216866
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
l : List α
⊢ drop n (drop 0 l) = drop (n + 0) l
simp