Produce eta-normal proofs

[RichardMoot]

Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to produce eta-normal proofs as well.

Add an (optional) proof transformation step which transforms long normal form proofs into beta-eta-normal proofs.