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

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