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 n : ℕ
ih : n + m ≃ m + n
⊢ step n + m ≃ m + step n
no goals