case nil
ι : Type ?u.45132
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l' : List α
h : [] ≠ []
⊢ tail ([] ++ l') = tail [] ++ l'

case cons
ι : Type ?u.45132
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l' : List α
head✝ : α
tail✝ : List α
h : head✝ :: tail✝ ≠ []
⊢ tail (head✝ :: tail✝ ++ l') = tail (head✝ :: tail✝) ++ l'
ι : Type ?u.45132
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l l' : List α
h : l ≠ []
⊢ tail (l ++ l') = tail l ++ l'
cases l
no goals
case nil
ι : Type ?u.45132
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l' : List α
h : [] ≠ []
⊢ tail ([] ++ l') = tail [] ++ l'
contradiction
no goals
case cons
ι : Type ?u.45132
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l' : List α
head✝ : α
tail✝ : List α
h : head✝ :: tail✝ ≠ []
⊢ tail (head✝ :: tail✝ ++ l') = tail (head✝ :: tail✝) ++ l'
simp