calc
  step (n + m) ≃ _ := Rel.symm Addition.step_add
  step n + m   ≃ _ := ‹step n + m ≃ step n + k›
  step n + k   ≃ _ := Addition.step_add
  step (n + k) ≃ _ := Rel.refl
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m k n : ℕ
ih : n + m ≃ n + k → m ≃ k
x✝ : step n + m ≃ step n + k
⊢ step (n + m) ≃ step (n + k)
no goals