match hxy : x == y, hyx : y == x with
| true, true => rfl
| true, false => rw [BEq.symm hxy] at hyx; contradiction
| false, true => rw [BEq.symm hyx] at hxy; contradiction
| false, false => rfl
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (x == y) = (y == x)
no goals