feat(kernel/converter): add eta-expansion to converter, this is important when terms contains metavariables

For example, consider the unification constrains

    fun (x : A), f (?m x)  =?=  f

Eta-reduction is not applicable since (?m x) is not a variable.
However, if we eta-expand the left-hand-side, we get

   fun (x : A), f (?m x)  =?=  fun (x : A), f x

which is reduced to

      (?m x) =?= x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(library/unifier): improve performance of instantiate_meta method

It provides a significant performance boost in some files.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(library/unifier): improve performance of instantiate_meta method