Rewriting does not generate existential variables

[gabrielhdt]

Rewriting generates holes that must be transformed into existential variables by the type checker. Unification hints have been adapted to use that mechanism.

Fixes issue #600

There is also a fix for the Dedukti export: pattern variable P with an environment [x] in the RHS would be printed as P x instead of (P x) (would cause issues with El P x v El (P x)).