very basic inversion funciton is working now. Because of circulatity (similar to what happened with terms) I moved some of the functions our of translation and into metaterm.

Translation of abstractions is not correct now as they will need to determine LF type of the variable.

Currently there are ecessive amounts of parenthesis but this can be changed in future.S
Translation: fix for invented proof term variables

- They should not have tag Nominal
- They should not all be "x"
- They should be suitably freshened

This version uses variables named "pt1", "pt2", ...