Auto-generalize variable's type declarations

* btl/pervasive.typer: Simplify declarations, relying on generalization.

* src/debruijn.ml (scope): Remove.
(meta_scope): New type alias.
(elab_context): Use it to add a map of known metavar names.
(empty_elab_context, ectx_new_scope): Handle the new metavar map.
(get_size): Add sanity check.

* src/elab.ml (meta_to_var, infer_and_generalize_type): New functions.
(lexp_decls_1): Use them to generalize var declarations.
(sform_identifier): Use new metavar map to handle names metavars.

* src/inverse_subst.ml (invertible, lookup_inv_subst)
(shift_inv_subst, compose_inv_subst, apply_inv_subst): New functions.

* src/lexp.ml (meta_id): New type alias.
(lexp): Use it.

* src/opslexp.ml (mv_set): Keep track of types, names, and (meta)scope.
(mv_set_union): Adjust accordingly.

* src/unification.ml (_unify_metavar): Use apply_inv_subst!