calc
  n₁     ≃ _ := Rel.symm AA.identR
  n₁ + 0 ≃ _ := ‹n₁ + 0 ≃ n₂ + 0›
  n₂ + 0 ≃ _ := AA.identR
  n₂     ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
this : n₁ + 0 ≃ n₂ + 0
⊢ n₁ ≃ n₂
no goals