ext
case mp
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z = 0
case mp.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.x = 0.x

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.y = 0.y