Your reasoning is faulty for two reasons. First, the transformation may not preserve the space complexity of the input (program size). So if a transformed progr

Your reasoning is faulty for two reasons. First, the transformation may not preserve the space complexity of the input (program size). So if a transformed program is exponentially bigger than the original, it is not equivalent from the prover's perspective. Second, even if the program size is preserved, the prover needs to write the proof. Finding a proof is a non-trivial problem, and there is no general mechanized way to do it. Therefore, we rely on human practice and intuition. It is therefore possible that human reasoning would work better in one formalism than another (although the avantage, if there is one, may change in favor of one formalism or the other depending on the specific problem, too). Now, I'm not saying either of these actually occurs, and it is possible the the two are more-or-less equivalent, but if so, it is not an immediate consequence of there being a transformation from one to the other.