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

case cons
ι : Type ?u.43325
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → tail (tail✝ ++ [a]) = tail tail✝ ++ [a]
h : head✝ :: tail✝ ≠ []
⊢ tail (head✝ :: tail✝ ++ [a]) = tail (head✝ :: tail✝) ++ [a]
ι : Type ?u.43325
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
h : l ≠ []
⊢ tail (l ++ [a]) = tail l ++ [a]
induction l
case cons
ι : Type ?u.43325
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → tail (tail✝ ++ [a]) = tail tail✝ ++ [a]
h : head✝ :: tail✝ ≠ []
⊢ tail (head✝ :: tail✝ ++ [a]) = tail (head✝ :: tail✝) ++ [a]
case nil
ι : Type ?u.43325
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
h : [] ≠ []
⊢ tail ([] ++ [a]) = tail [] ++ [a]

case cons
ι : Type ?u.43325
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → tail (tail✝ ++ [a]) = tail tail✝ ++ [a]
h : head✝ :: tail✝ ≠ []
⊢ tail (head✝ :: tail✝ ++ [a]) = tail (head✝ :: tail✝) ++ [a]
contradiction
no goals
case cons
ι : Type ?u.43325
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → tail (tail✝ ++ [a]) = tail tail✝ ++ [a]
h : head✝ :: tail✝ ≠ []
⊢ tail (head✝ :: tail✝ ++ [a]) = tail (head✝ :: tail✝) ++ [a]
rw [tail, cons_append, tail]