case nil
ι : Type ?u.42548
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
t : List α
h : [] ≠ []
⊢ head! ([] ++ t) = head! []

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

case cons
ι : Type ?u.42548
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → head! (tail✝ ++ t) = head! tail✝
h : head✝ :: tail✝ ≠ []
⊢ head! (head✝ :: tail✝ ++ t) = head! (head✝ :: tail✝)
contradiction
no goals
case cons
ι : Type ?u.42548
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → head! (tail✝ ++ t) = head! tail✝
h : head✝ :: tail✝ ≠ []
⊢ head! (head✝ :: tail✝ ++ t) = head! (head✝ :: tail✝)
rfl