ι : Type ?u.89110
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
h : length [] - 1 < length []
⊢ False
ι : Type ?u.89110
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
h : length l - 1 < length l
⊢ l ≠ []
rintro rfl
no goals
ι : Type ?u.89110
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
h : length [] - 1 < length []
⊢ False
exact Nat.lt_irrefl 0 h