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