feat(library/basic_thms): add Refute theorem

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/basic_thms): simplify DoubleNegElim

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel): incorrect use of scoped_map

This commit also adds a new test that exposes the problem.
The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/type_inferer): another incorrect use of scoped_map

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean): add ExistsElim test

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