- 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

Discard pvs2k script, use a lisp function
Discard logging, use trace instead
Discard to-dk3 and rely on pp-dk

- add the encoding of the cast,
- update translator

- update translator
- update tests
- update ci (to use correct lambdapi version)

- less useless printing
- simplified type printing

Do not unfold definition, remove code that compiles recursive
definitions to recursors

require open into require