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

case cons
ι : Type ?u.29930
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = getLast tail✝ h
h✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = getLast (head✝ :: tail✝) h✝
ι : Type ?u.29930
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
⊢ ∀ (h : l ≠ []), getLast (a :: l) (_ : a :: l ≠ []) = getLast l h
induction l <;> intros
case cons
ι : Type ?u.29930
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = getLast tail✝ h
h✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = getLast (head✝ :: tail✝) h✝
case nil
ι : Type ?u.29930
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
h✝ : [] ≠ []
⊢ getLast [a] (_ : [a] ≠ []) = getLast [] h✝

case cons
ι : Type ?u.29930
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = getLast tail✝ h
h✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = getLast (head✝ :: tail✝) h✝
contradiction
no goals
case cons
ι : Type ?u.29930
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h : tail✝ ≠ []), getLast (a :: tail✝) (_ : a :: tail✝ ≠ []) = getLast tail✝ h
h✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) (_ : a :: head✝ :: tail✝ ≠ []) = getLast (head✝ :: tail✝) h✝
rfl