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