Use mathport translations

[siddhartha-gadgil]

Eventually the Lean 3 -> Lean 4 translation should be done by using mathport.

[0art0]

A working set-up is available on the mathport branch. The script mathport-init.sh can be used to set up mathport for translation (assuming mathport is a dependency of the repository).

The example mathport-translation-example.sh is a test example for benchmarking. It currently takes about 18-19 seconds to run, which is too slow to be useful in practice.

[siddhartha-gadgil]

@0art0 I don't mean using mathport as a program but as a library, i.e., instead of using my ad hoc translation with dictionary etc the funcStr is translated the way a term will be translated during mathport.

[siddhartha-gadgil]

This is done now.