Theorem: LoVe.Set.Mem_singleton (LoVe/LoVelib.lean)

State before:
α : Type
a b : α
⊢ a ∈ {b} ↔ a = b
Tactic:
rfl
State after:
no goals