Update to lambdapi 2 (which uses a new coercion insertion algorithm)

New typechecker requires more resources in some cases

- add a patch (by Sam) to have a prove-formula function in PVS
- remove "opaque" keyword because of issue 830 of lambdapi,
- added some encoding facilities to write proofs
- export has a switch to translate proofs

General simplifications

Do not remember types in context anymore

Fix tests (call correct function), fix some newlines printing