- If you don't check that the translation is good,
then there is every chance that either:
- the proofs you carry out in your rich system do not correspond naturally to proofs in Z_2;
- your rich system does not share the same consequence relation as Z_2;

- I can't say what the best books are, since I picked up most of what I know from fairly obscure sources. The text I have read that gives the best feel of what life is like in a a proof theory based on the lambda calculus is Jean-Yves Girard's `Proofs and Types' (with appendices by Paul Taylor and Yves Lafont). This text gives many of the most important results, in particular the proof of strong normalisation for System F and Martin-Loef's demonstration that this SN result is equivalent to the consistency of SOA, but be warned that this text is challenging, cavalier about definitions and has a very non-mainstream agenda. Also the book does not explain why polymorphism is not set-theoretic; for this I recommend John Reynold's orginal paper.