quotient.eq

Stream: general

[Patrick Massot]

We have

@[simp] theorem quotient.eq [r : setoid α] {x y : α} : ⟦x⟧ = ⟦y⟧ ↔ x ≈ y :=
⟨quotient.exact, quotient.sound⟩

Are we sure this is a good simp lemma?