rw [BEq.symm hyx] at hxy
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (x == y) = false
hyx : (y == x) = true
⊢ false = true
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : true = false
hyx : (y == x) = true
⊢ false = true