Adding inversion of LF terms.
Fix term_to_string
Testing the translation at the OCaml level
Remove dependency on findlib for "make top"
Revert "Remove dependency on findlib for "make top""

This reverts commit 8aff878399e0134d862d7906c5d0c8e30e3f53e7.
Add support for parsing .elf specifications.

See examples/elf/test.thm
Very basic inversion function 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 excessive 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 "lfx1", "lfx2", ...
Fix incorrect new basic types from Abella.read_elf_specification
Fixed the proof in elf/test.elf.

That file should be renamed soon.
Keep the unprocessed LF spec signature in Prover.lf_sign
Add a framework for pretty printing
Make the term printer pluggable
Starting to update the LF printer
Finish the implementation of the simple-minded inverter.
Also fixes the types
Type-directed merging of Obj and LFObj using an extra "obj_logic" parameter
An unfinished version of the uniqueness example
Finishing the type uniqueness proof
Minor pretty printing cleanup