apply ind_on (motive := λ n => n + step m ≃ step (n + m)) n
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + step m ≃ step (n + m)
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + step m ≃ step (0 + m)

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + step m ≃ step (m_1 + m) → step m_1 + step m ≃ step (step m_1 + m)