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

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