1, the sufficiency of a priori proof:? x(F(x)∧? y(G(y)→H(x,y)))→? x? y(F(x)∧(G(y)→H(x,y)))
( 1)? x(F(x)∧? y(G(y)→H(x,y))) P
(2)P F(α)∧? y(G(y)→H(α,y))? -( 1)
(3)P? y(G(y)→H(α,y)) T(2)
(4)P G(y)→H(α,y)? -(3)
(5)P F(α) T(2)
(6)P F(α)∧(G(y)→H(α,y) ) T(4)(5)
(7)P? y(F(α)∧(G(y)→H(α,y)))? +(6)
(8)P? x? y(F(x)∧(G(y)→H(x,y)))? +(7)
(9){} ? x(F(x)∧? y(G(y)→H(x,y)))→? x? y(F(x)∧(G(y)→H(x,y))) D( 1)(8)
2. The necessity of recertification: x? y(F(x)∧(G(y)→H(x,y)))→? x(F(x)∧? y(G(y)→H(x,y)))
( 1)P? x? y(F(x)∧(G(y)→H(x,y))) P
(2)P? y(F(α)∧(G(y)→H(α,y)))? -( 1)
(3)P F(α)∧(G(y)→H(α,y))? -(2)
(4)P G(y)→H(α,y) T(2)
(5)P? y(G(y)→H(α,y))? +(4)
(6)P F(α) T(2)
(7)P F(α)∧? y(G(y)→H(α,y)) T(5)(6)
(8)P? x? y(F(x)∧(G(y)→H(x,y)))? +(7)
(9){} ? x? y(F(x)∧(G(y)→H(x,y)))→? x(F(x)∧? y(G(y)→H(x,y))D( 1)(8)
So it can be proved that they are equivalent.