ι : Type ?u.31925
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ getLast l₂ h₁ = getLast l₂ h₂
ι : Type ?u.31925
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
h₁ : l₁ ≠ []
h₂ : l₂ ≠ []
h₃ : l₁ = l₂
⊢ getLast l₁ h₁ = getLast l₂ h₂
subst l₁
no goals
ι : Type ?u.31925
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ getLast l₂ h₁ = getLast l₂ h₂
rfl