case nil
ι : Type ?u.42760
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ t : List α
x : α
h : x ∈ head? []
⊢ x ∈ head? ([] ++ t)

case cons
ι : Type ?u.42760
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ t : List α
x head✝ : α
tail✝ : List α
h : x ∈ head? (head✝ :: tail✝)
⊢ x ∈ head? (head✝ :: tail✝ ++ t)
ι : Type ?u.42760
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ s t : List α
x : α
h : x ∈ head? s
⊢ x ∈ head? (s ++ t)
cases s
case cons
ι : Type ?u.42760
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ t : List α
x head✝ : α
tail✝ : List α
h : x ∈ head? (head✝ :: tail✝)
⊢ x ∈ head? (head✝ :: tail✝ ++ t)
case nil
ι : Type ?u.42760
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ t : List α
x : α
h : x ∈ head? []
⊢ x ∈ head? ([] ++ t)

case cons
ι : Type ?u.42760
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ t : List α
x head✝ : α
tail✝ : List α
h : x ∈ head? (head✝ :: tail✝)
⊢ x ∈ head? (head✝ :: tail✝ ++ t)
contradiction
no goals
case cons
ι : Type ?u.42760
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ t : List α
x head✝ : α
tail✝ : List α
h : x ∈ head? (head✝ :: tail✝)
⊢ x ∈ head? (head✝ :: tail✝ ++ t)
exact h