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 n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
⊢ ∀ (m_1 : ℕ), step n₁ ≃ step m_1 → step n₁ + m ≃ step m_1 + m
no goals