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

State before:
α : Type
a : α
P : α → Prop
⊢ a ∈ {a | P a} ↔ P a
Tactic:
rfl
State after:
no goals