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