Your rewrite seems to have the same error as the previous version. A correct formalization of Wei’s solution could look like this:
A1 ⊢ ∀P. (A1 ⊢ P) ↔ (A2 ⊢ P)
If A1=A2, that equation collapses into a tautology, as it should.
Your rewrite seems to have the same error as the previous version. A correct formalization of Wei’s solution could look like this:
A1 ⊢ ∀P. (A1 ⊢ P) ↔ (A2 ⊢ P)
If A1=A2, that equation collapses into a tautology, as it should.