α : Type u_1
β : Type ?u.2600
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ drop 1 l <:+ l
α : Type u_1
β : Type ?u.2600
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tail l <:+ l
rw [← drop_one]
no goals
α : Type u_1
β : Type ?u.2600
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ drop 1 l <:+ l
apply drop_suffix