apply AA.subst₁
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ from_prod (a₁ + b₁, a₂ + b₂) ≃ from_prod (b₁ + a₁, b₂ + a₂)
case a
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ : ℕ
⊢ (a₁ + b₁, a₂ + b₂) ≃ (b₁ + a₁, b₂ + a₂)