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>