It seems like in your first part, you're saying that proofs are the same as their normalized proofs, up to some rewriting system. So like how we say 3-2 is the

It seems like in your first part, you're saying that proofs are the same as their normalized proofs, up to some rewriting system. So like how we say 3-2 is the same as 1, basically, or (more interestingly) saying that x-x is the same as zero, or that e^(i pi (2n+1)) is the same as -1. Yes, they can be reduced/normalized to the same thing, but in basically any system with terms, `reduction(term)` is not always the same as `term`, And 'a sequence of term transformations' is a common proof method. There's obviously a sense in which they're the same, but at the proof level, I would be surprised if that's a particularly useful sense, because the whole point of a proof is that it's the journey, not the destination. Even within the same "level," in your terms.