case nil
α : Type u_1
a : α
h₁✝ : [a] ≠ []
h₂✝ : [] ≠ []
⊢ getLast [a] h₁✝ = getLast [] h₂✝

case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h₁ : a :: tail✝ ≠ []) (h₂ : tail✝ ≠ []), getLast (a :: tail✝) h₁ = getLast tail✝ h₂
h₁✝ : a :: head✝ :: tail✝ ≠ []
h₂✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) h₁✝ = getLast (head✝ :: tail✝) h₂✝
α : Type u_1
a : α
l : List α
⊢ ∀ (h₁ : a :: l ≠ []) (h₂ : l ≠ []), getLast (a :: l) h₁ = getLast l h₂
induction l <;> intros
case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h₁ : a :: tail✝ ≠ []) (h₂ : tail✝ ≠ []), getLast (a :: tail✝) h₁ = getLast tail✝ h₂
h₁✝ : a :: head✝ :: tail✝ ≠ []
h₂✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) h₁✝ = getLast (head✝ :: tail✝) h₂✝
case nil
α : Type u_1
a : α
h₁✝ : [a] ≠ []
h₂✝ : [] ≠ []
⊢ getLast [a] h₁✝ = getLast [] h₂✝

case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h₁ : a :: tail✝ ≠ []) (h₂ : tail✝ ≠ []), getLast (a :: tail✝) h₁ = getLast tail✝ h₂
h₁✝ : a :: head✝ :: tail✝ ≠ []
h₂✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) h₁✝ = getLast (head✝ :: tail✝) h₂✝
{contradiction}
no goals
case cons
α : Type u_1
a head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (h₁ : a :: tail✝ ≠ []) (h₂ : tail✝ ≠ []), getLast (a :: tail✝) h₁ = getLast tail✝ h₂
h₁✝ : a :: head✝ :: tail✝ ≠ []
h₂✝ : head✝ :: tail✝ ≠ []
⊢ getLast (a :: head✝ :: tail✝) h₁✝ = getLast (head✝ :: tail✝) h₂✝
rfl