Generalize `Identity` with `Identity o` where the old
`Identity` is now `Identity 0` and `Identity o` is like the old
`Shift (Identity, o)`.

(mkShift): Use `Identity` when possible.
(shift): Use `Identity`.
(identity): Adjust to new `Identity`.
(lookup, identity_p, compose): Generalize to the new `Identity o`.
(substitute): Use `identity`.

* src/elab.ml (newMetavar): Use S.identity.

* src/inverse_subst.ml (is_identity): Take advantage of the new `Identity o`.
(shift_inv_subst): Optimize the case when n is 0.
(transfo, invertible, lookup_inv_subst, compose_inv_subst):
Generalize to the new `Identity o`.

* src/lexp.ml (subst_string): Handle the new `Identity o`.
(subst_eq): Generalize to the new `Identity o`.

* tests/inverse_test.ml (is_identity): Copy new def from inverse_subst.ml.

* tests/unify_test.ml (generate_testable): Use `identity`.

Fold `Shift` into the `Cons`, and hence remove `Shift` since it's not needed
as a separate constructor any more.

(sink, substitute): Use `cons`
(lookup, mkShift, cons, compose):
* src/lexp.ml (subst_string, subst_eq):
* src/inverse_subst.ml (transfo, is_identity, invertible)
(lookup_inv_subst, compose_inv_subst): Adjust accordingly.

* tests/inverse_test.ml (is_identity): Update from src/inverse_subst.ml.

* src/opslexp.ml (lexp_whnf): Use `S.cons`.