case step =>
  intro n₁ (ih : ∀ y, n₁ ≃ y → n₁ + m ≃ y + m) n₂
  show step n₁ ≃ n₂ → step n₁ + m ≃ n₂ + m
  apply cases_on (motive := λ y => step n₁ ≃ y → step n₁ + m ≃ y + m)
  case zero =>
    intro (_ : step n₁ ≃ 0)
    show step n₁ + m ≃ 0 + m
    exact absurd ‹step n₁ ≃ 0› step_neqv_zero
  case step =>
    intro n₂ (_ : step n₁ ≃ step n₂)
    show step n₁ + m ≃ step n₂ + m
    have : n₁ ≃ n₂ := AA.inject ‹step n₁ ≃ step n₂›
    calc
      step n₁ + m   ≃ _ := Addition.step_add
      step (n₁ + m) ≃ _ := AA.subst₁ (ih _ ‹n₁ ≃ n₂›)
      step (n₂ + m) ≃ _ := Rel.symm Addition.step_add
      step n₂ + m   ≃ _ := Rel.refl
ℕ : 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
no goals