case step =>
  intro n (ih : n + m ≃ m + n)
  show step n + m ≃ m + step n
  calc
    step n + m   ≃ _ := Addition.step_add
    step (n + m) ≃ _ := AA.subst₁ ih
    step (m + n) ≃ _ := Rel.symm add_step
    m + step n   ≃ _ := Rel.refl
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + m ≃ m + m_1 → step m_1 + m ≃ m + step m_1
no goals