α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ ⟦AList.singleton y b⟧ ↔ x = y
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ singleton y b ↔ x = y
simp only [singleton]
no goals
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ ⟦AList.singleton y b⟧ ↔ x = y
erw [mem_cons, mem_nil_iff, or_false_iff]