case x_2
ι : Type ?u.28091
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ b :: l = [] → False
ι : Type ?u.28091
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ length (dropLast (a :: b :: l)) = length (a :: b :: l) - 1
rw [dropLast, length_cons, length_cons, length_dropLast (b::l), succ_sub_one, length_cons,
  succ_sub_one]
no goals
case x_2
ι : Type ?u.28091
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ b :: l = [] → False
simp