Theorem: LoVe.mem_Id (LoVe/LoVelib.lean)

State before:
α : Type
a b : α
⊢ (a, b) ∈ Id ↔ b = a
Tactic:
rfl
State after:
no goals