fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): add flag for enabling/disabling expensive extensions in the unifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/pp): do not display metavariable arguments by default, add option pp.metavar_args to control whether they are displayed or not

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>