no goals
ι : Type ?u.34045
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ Option.isNone (getLast? []) = true ↔ [] = []
simp
no goals
ι : Type ?u.34045
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
⊢ Option.isNone (getLast? [a]) = true ↔ [a] = []
simp
no goals
ι : Type ?u.34045
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ Option.isNone (getLast? (a :: b :: l)) = true ↔ a :: b :: l = []
simp [@getLast?_isNone (b :: l)]