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