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

State before:
α : Type
A : Set α
⊢ {a | a ∈ A} = A
Tactic:
rfl
State after:
no goals