refactor(library/unifier): add is_def_eq alias

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): add support for unification constraints of the form "(elim ... (?m ...)) =?= t", where elim is an eliminator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add pairs

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