intro hxy
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
⊢ (x == y) = true → (z == x) = (z == y)
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
⊢ (z == x) = (z == y)