Unit tests on the translator

Create the universal closure if it does not exist already

Should fail for the moment

Allows to typecheck KernelDefinition

More uniform processing, at the cost of the encoding of 'restrict'
and 'extend' and not processing K_props and identity_props (they use
S_pred things).

Replaced 'purify.pl' by a command of 'psnj'. Theories are described by
a JSON file.

Rework hierarchy of project (mainly all PVS patches in a same directory)

Moved
- specs/tools/prelude to prelude,
- prelude patches to prelude/patches/
- the "simple" theory to tests/thy_translation/"
- scripts are moved to scripts/

Enable check in more tests

No need for files "load.lp" or "rules.lp", they are statically generated
by the pipe.

Renamed qfo into meta
Renamed library roots from qfo to psnj
Renamed pipeline libroot from qfo to pipe

The name qfo remains for the moment and dkmeta has been re implemented
in lambdapi

alt-ergo and run why3 config detect

Contains several tests with
- implication on LHS of implication (A -> B) -> C
- universal quantification in LHS of implication (all x P) -> C