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