Coercions on dependent tuples as well as from non dependent tuples to
dependent tuples

To avoid leaving altered global variables when pp-dk finishes

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