Delift used to produce not well typed substitutions. In turn, this

Delift used to produce not well typed substitutions. In turn, this
led to tactics that were not failing immediately, but only at Qed.

Fixed by adding the appropriate check to the delift function.

Note:
 - pass the metavariable number (-1) to avoid the check when you know what
   you are doing (e.g. when delift is just used to restrict a term or to
   replace a term with a convertible one). This used to be 0 (not -1).
 - in some cases (algebraic universes and implicits used to stop chains of
   metavariables) the check is relaxed
 - to make the CerCo script pass (in very "reasonable" and "frequent" cases),
   the algorithm needs to solve the following unification problem:
     S (?[n]) == ?[(S n)]
   Our algorithm used to delift S(?[n]) w.r.t. (S n), yielding x |- ? := x.
   By chance, this was the right solution since S (?[n]) becomes (S n) and
   also ?[(S n)] becomes (S n). However, the two solutions were both added
   to the subst (first bug) and they could even be different (second bug).
   We fix this by checking that they are not different.
   However, at the moment, the solution still occurs twice in the subst....