calc
  step n + step m     ≃ _ := Addition.step_add
  step (n + step m)   ≃ _ := AA.subst₁ ih
  step (step (n + m)) ≃ _ := AA.subst₁ (Rel.symm Addition.step_add)
  step (step n + m)   ≃ _ := Rel.refl
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
ih : n + step m ≃ step (n + m)
⊢ step n + step m ≃ step (step n + m)
no goals