left
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true ∨ (!x✝) = true
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
hxy : (!x == y) = true
z : α
x✝ : Bool
hxz : (x == z) = false
hyz : (z == y) = x✝
⊢ (!false) = true