refactor(kernel/metavar): separate substitution from their justifications

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/metavar): expose destructive assign

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): 'forget' justifications after finding a solution, the justifications are only needed inside the unifier (for implementing nonchronological backtracking)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/standard): use inductive datatype to define inhabited

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/standard): congr1 and congr2 theorem definition, we should allow A and B to inhabit different universes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/notation_cmd): fix default, add 'prev' action

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/notation_cmd): reuse existing precedence to increase compatibility with existing notation

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