no goals
ι : Type ?u.487859
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
⊢ ilast' a [] ∈ [a]
simp [ilast']
ι : Type ?u.487859
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ ilast' a (b :: l) = a ∨ ilast' a (b :: l) ∈ b :: l
ι : Type ?u.487859
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ ilast' a (b :: l) ∈ a :: b :: l
rw [mem_cons]
no goals
ι : Type ?u.487859
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ ilast' a (b :: l) = a ∨ ilast' a (b :: l) ∈ b :: l
exact Or.inr (ilast'_mem b l)