exact absurd ‹step (n + m) ≃ 0› step_neqv_zero
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this✝ : step (n + m) ≃ step n + m
this : step (n + m) ≃ 0
⊢ False
no goals