Theorem: LoVe.UPair.Setoid_Iff (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
α : Type
ab₁ ab₂ : α × α
⊢ ab₁ ≈ ab₂ ↔ {ab₁.fst, ab₁.snd} = {ab₂.fst, ab₂.snd}
Tactic:
rfl
State after:
no goals