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

State before:
α : Type
a : α
⊢ a ∈ ∅ ↔ False
Tactic:
simp [Membership.mem, Set.Mem, EmptyCollection.emptyCollection]
State after:
no goals