case step =>
  intro n (_ : Positive (step n))
  exists n
  show step n ≃ step n
  exact Rel.refl
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ ∀ (m : ℕ), Positive (step m) → ∃ m_1, step m_1 ≃ step m
no goals