rw [BEq.trans hzx hxy] at hzy
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = true
hzy : (z == y) = false
⊢ true = false
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y z : α
hxy : (x == y) = true
hzx : (z == x) = true
hzy : true = false
⊢ true = false