In this post, Andrej Bauer says:
There is a theorem about normal forms of proofs in intuitionistic logic which tells us that every proof of a negation can be rearranged so that it ends with the inference rule cited above
Can someone point me to a text on "normal forms of proofs in intuitionistic logic" and to this theorem?