apply ind_on (motive := λ x => ∀ y, x ≃ y → x + m ≃ y + m) n₁
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂ m : ℕ
⊢ n₁ ≃ n₂ → n₁ + m ≃ n₂ + m
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 + m ≃ y + m

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