Since the HOL Peano numbers theory includes simple function types with cause notation clashes with dependent function types.

Also postpend "_conj" to all conjectures/axioms for easy recognition in output of tptp exporter.

This makes the examples look better when viewed from a web browser

TODOs:
- find better file names,
- subfolders for category theory examples
- rewrite overview file

Additionally improve the treatment of nested abbreviations in the translation implementation.

It now additionally introduces injectivity/surjectivity/bijectivity inverses
and lemmas (proven by the hammer) relating them.

Interestingly neither LEO nor Zipperp'n can solve this within 60s timeout.
However, the MMT based prover can solve this. Maybe the handwritten example is not ideally formatted, or maybe MMTs internal solver helps here.

Also modify build script to only look at folder with MMT examples.