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