fix(library/fo_unify): unify (?f ?x) with (g a b)

We flat applications. So, (g a b) is actually ((g a) b).
So, we must be able to unify (?f ?x) with (g a b).
Solution:
        ?g <- (g a)
        ?x <- b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer

The idea is to make it an optional parameter independent of metavar_env.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/parser): cleanup tactic support in the default lean parser

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac)