diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean
index 11aac6cfec..d98449e5b4 100644
--- a/library/init/data/int/order.lean
+++ b/library/init/data/int/order.lean
@@ -193,7 +193,7 @@ iff.mpr
   (int.lt_iff_le_and_ne _ _)
   (and.intro hac (assume heq, int.not_le_of_gt begin rw heq, exact hbc end hab))
 
-instance : linear_ordered_ring int :=
+instance : decidable_linear_ordered_comm_ring int :=
 { int.comm_ring with
   le              := int.le,
   le_refl         := int.le_refl,
@@ -211,7 +211,13 @@ instance : linear_ordered_ring int :=
   mul_pos         := @int.mul_pos,
   le_iff_lt_or_eq := int.le_iff_lt_or_eq,
   le_total        := int.le_total,
-  zero_lt_one     := int.zero_lt_one }
+  zero_lt_one     := int.zero_lt_one,
+  decidable_eq    := int.decidable_eq,
+  decidable_le    := int.decidable_le,
+  decidable_lt    := int.decidable_lt }
+
+instance : decidable_linear_ordered_comm_group int :=
+by apply_instance
 
 end int
 
diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index 733812ab51..d0cd58fd92 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -35,6 +35,8 @@ match env^.get d with
 | exceptional.success _      := tt
 | exceptional.exception ._ _ := ff
 end
+/- Return tt iff the given name is a namespace -/
+meta constant is_namespace    : environment → name → bool
 /- Add a new inductive datatype to the environment
    name, universe parameters, number of parameters, type, constructors (name and type), is_meta -/
 meta constant add_inductive   : environment → name → list name → nat → expr → list (name × expr) → bool →
diff --git a/library/smt/arith.lean b/library/smt/arith.lean
index 1abc311e11..432e3af8d2 100644
--- a/library/smt/arith.lean
+++ b/library/smt/arith.lean
@@ -1,17 +1,21 @@
--- TODO(Leo): remove after we port reals to new stdlib
--- Arithmetic
+-- TODO(Leo): remove after we port reals to new stdlib and add int.has_div and int.has_mod
+constants (int.has_div : has_div int)
+constants (int.has_mod : has_mod int)
+
+attribute [instance] int.has_div int.has_mod
+
 constants (real : Type)
 
-constants (real_has_zero : has_zero real)
-constants (real_has_one : has_one real)
-constants (real_has_add : has_add real)
-constants (real_has_mul : has_mul real)
-constants (real_has_sub : has_sub real)
-constants (real_has_neg : has_neg real)
-constants (real_has_div : has_div real)
-constants (real_has_lt : has_lt real)
-constants (real_has_le : has_le real)
+constants (real.has_zero : has_zero real)
+constants (real.has_one : has_one real)
+constants (real.has_add : has_add real)
+constants (real.has_mul : has_mul real)
+constants (real.has_sub : has_sub real)
+constants (real.has_neg : has_neg real)
+constants (real.has_div : has_div real)
+constants (real.has_lt : has_lt real)
+constants (real.has_le : has_le real)
 
-attribute [instance] real_has_zero real_has_one real_has_add real_has_mul real_has_sub real_has_neg real_has_div real_has_le real_has_lt
+attribute [instance] real.has_zero real.has_one real.has_add real.has_mul real.has_sub real.has_neg real.has_div real.has_le real.has_lt
 
 constants (real.of_int : int → real) (real.to_int : real → int) (real.is_int : real → Prop)
diff --git a/script/gen_constants_cpp.py b/script/gen_constants_cpp.py
index 5b6bdcbabb..9499e2e04b 100644
--- a/script/gen_constants_cpp.py
+++ b/script/gen_constants_cpp.py
@@ -36,6 +36,7 @@ def main(argv=None):
     basename, ext = os.path.splitext(infile)
     cppfile       = basename + ".cpp"
     hfile         = basename + ".h"
+    tst_file      = "../../tests/lean/run/check_" + basename + ".lean"
     constants     = []
     with open(infile, 'r') as f:
         for line in f:
@@ -82,6 +83,14 @@ def main(argv=None):
             f.write('name const & get_%s_name() { return *g_%s; }\n' % (c[0], c[0]))
         # end namespace
         f.write('}\n')
+    with open(tst_file, 'w') as f:
+        f.write('-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n')
+        f.write("import smt system.io\n")
+        f.write("open tactic\n");
+        f.write("meta def script_check_id (n : name) : tactic unit :=\n");
+        f.write("do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail (\"identifier '\" ++ to_string n ++ \"' is not a constant, namespace nor attribute\")\n");
+        for c in constants:
+            f.write("run_command script_check_id `%s\n" % c[1])
     print("done")
     return 0
 
diff --git a/src/frontends/smt2/elaborator.cpp b/src/frontends/smt2/elaborator.cpp
index 4f053f8035..ce5db13aaa 100644
--- a/src/frontends/smt2/elaborator.cpp
+++ b/src/frontends/smt2/elaborator.cpp
@@ -110,7 +110,6 @@ static expr mk_chainable_app(buffer<expr> const & args) {
 // TODO(dhs): use a macro for this? It scales quadratically.
 // At this stage in elaboration: ["@distinct A", arg1, ... ,argN]
 static expr mk_distinct_app(buffer<expr> const & args) {
-    lean_assert(is_constant(app_fn(args[0])) && const_name(app_fn(args[0])) == get_distinct_name());
     unsigned num_args = args.size() - 1;
     if (num_args == 1)
         return mk_constant(get_true_name());
@@ -158,9 +157,8 @@ private:
     }
 
     expr elaborate_distinct(buffer<expr> & args) {
-        lean_assert(is_constant(args[0]) && const_name(args[0]) == get_distinct_name());
         expr ty = m_tctx.infer(args[1]);
-        args[0] = mk_app(mk_constant(get_distinct_name(), {l1()}), ty);
+        args[0] = mk_app(mk_constant(get_ne_name(), {l1()}), ty);
         return mk_distinct_app(args);
     }
 
@@ -182,7 +180,6 @@ private:
     }
 
     expr elaborate_select(buffer<expr> & args) {
-        lean_assert(is_constant(args[0]) && const_name(args[0]) == get_select_name());
         expr ty = m_tctx.infer(args[1]);
         buffer<expr> array_args;
         expr array = get_app_args(ty, array_args);
@@ -192,7 +189,6 @@ private:
     }
 
     expr elaborate_store(buffer<expr> & args) {
-        lean_assert(is_constant(args[0]) && const_name(args[0]) == get_store_name());
         expr ty = m_tctx.infer(args[1]);
         buffer<expr> array_args;
         expr array = get_app_args(ty, array_args);
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 0e01f61b79..704e088270 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -23,7 +23,6 @@ name const * g_bool = nullptr;
 name const * g_bool_ff = nullptr;
 name const * g_bool_tt = nullptr;
 name const * g_bind = nullptr;
-name const * g_bv = nullptr;
 name const * g_caching_user_attribute = nullptr;
 name const * g_cast = nullptr;
 name const * g_cast_eq = nullptr;
@@ -44,13 +43,10 @@ name const * g_comm_semiring = nullptr;
 name const * g_congr = nullptr;
 name const * g_congr_arg = nullptr;
 name const * g_congr_fun = nullptr;
-name const * g_cyclic_numerals = nullptr;
-name const * g_cyclic_numerals_bound = nullptr;
 name const * g_decidable = nullptr;
 name const * g_decidable_by_contradiction = nullptr;
 name const * g_decidable_to_bool = nullptr;
 name const * g_discrete_field = nullptr;
-name const * g_distinct = nullptr;
 name const * g_distrib = nullptr;
 name const * g_dite = nullptr;
 name const * g_div = nullptr;
@@ -62,13 +58,9 @@ name const * g_Exists = nullptr;
 name const * g_eq = nullptr;
 name const * g_eq_cases_on = nullptr;
 name const * g_eq_drec = nullptr;
-name const * g_eq_elim_inv_inv = nullptr;
-name const * g_eq_intro = nullptr;
 name const * g_eq_mp = nullptr;
 name const * g_eq_mpr = nullptr;
-name const * g_eq_nrec = nullptr;
 name const * g_eq_rec = nullptr;
-name const * g_eq_rec_eq = nullptr;
 name const * g_eq_refl = nullptr;
 name const * g_eq_subst = nullptr;
 name const * g_eq_symm = nullptr;
@@ -182,18 +174,11 @@ name const * g_is_associative = nullptr;
 name const * g_is_associative_assoc = nullptr;
 name const * g_is_commutative = nullptr;
 name const * g_is_commutative_comm = nullptr;
-name const * g_is_int = nullptr;
-name const * g_is_trunc_is_prop = nullptr;
-name const * g_is_trunc_is_prop_elim = nullptr;
-name const * g_is_trunc_is_set = nullptr;
 name const * g_ite = nullptr;
 name const * g_left_distrib = nullptr;
 name const * g_left_comm = nullptr;
 name const * g_le = nullptr;
 name const * g_le_refl = nullptr;
-name const * g_lift = nullptr;
-name const * g_lift_down = nullptr;
-name const * g_lift_up = nullptr;
 name const * g_linear_ordered_comm_ring = nullptr;
 name const * g_linear_ordered_ring = nullptr;
 name const * g_linear_ordered_semiring = nullptr;
@@ -201,11 +186,6 @@ name const * g_list = nullptr;
 name const * g_list_nil = nullptr;
 name const * g_list_cons = nullptr;
 name const * g_lt = nullptr;
-name const * g_map = nullptr;
-name const * g_map_insert = nullptr;
-name const * g_map_lookup = nullptr;
-name const * g_map_select = nullptr;
-name const * g_map_store = nullptr;
 name const * g_match_failed = nullptr;
 name const * g_mod = nullptr;
 name const * g_monad = nullptr;
@@ -231,7 +211,6 @@ name const * g_nat_has_add = nullptr;
 name const * g_nat_has_mul = nullptr;
 name const * g_nat_has_div = nullptr;
 name const * g_nat_has_sub = nullptr;
-name const * g_nat_has_neg = nullptr;
 name const * g_nat_has_lt = nullptr;
 name const * g_nat_has_le = nullptr;
 name const * g_nat_add = nullptr;
@@ -362,30 +341,23 @@ name const * g_put_nat = nullptr;
 name const * g_to_pexpr = nullptr;
 name const * g_quot_mk = nullptr;
 name const * g_quot_lift = nullptr;
-name const * g_rat_divide = nullptr;
-name const * g_rat_of_num = nullptr;
-name const * g_rat_of_int = nullptr;
 name const * g_real = nullptr;
-name const * g_real_has_zero = nullptr;
-name const * g_real_has_one = nullptr;
+name const * g_real_of_int = nullptr;
+name const * g_real_to_int = nullptr;
+name const * g_real_is_int = nullptr;
+name const * g_real_has_neg = nullptr;
+name const * g_real_has_div = nullptr;
 name const * g_real_has_add = nullptr;
 name const * g_real_has_mul = nullptr;
 name const * g_real_has_sub = nullptr;
-name const * g_real_has_div = nullptr;
-name const * g_real_has_le = nullptr;
 name const * g_real_has_lt = nullptr;
-name const * g_real_has_neg = nullptr;
-name const * g_real_is_int = nullptr;
-name const * g_real_of_rat = nullptr;
-name const * g_real_of_int = nullptr;
-name const * g_real_to_int = nullptr;
+name const * g_real_has_le = nullptr;
 name const * g_rfl = nullptr;
 name const * g_right_distrib = nullptr;
 name const * g_ring = nullptr;
 name const * g_scope_trace = nullptr;
 name const * g_set_of = nullptr;
 name const * g_sep = nullptr;
-name const * g_select = nullptr;
 name const * g_semiring = nullptr;
 name const * g_sigma = nullptr;
 name const * g_sigma_cases_on = nullptr;
@@ -398,18 +370,12 @@ name const * g_psigma_mk = nullptr;
 name const * g_psigma_fst = nullptr;
 name const * g_psigma_snd = nullptr;
 name const * g_simp = nullptr;
-name const * g_simplifier_assoc_subst = nullptr;
-name const * g_simplifier_congr_bin_op = nullptr;
-name const * g_simplifier_congr_bin_arg1 = nullptr;
-name const * g_simplifier_congr_bin_arg2 = nullptr;
-name const * g_simplifier_congr_bin_args = nullptr;
 name const * g_singleton = nullptr;
 name const * g_sizeof = nullptr;
 name const * g_smt_array = nullptr;
 name const * g_smt_select = nullptr;
 name const * g_smt_store = nullptr;
 name const * g_smt_prove = nullptr;
-name const * g_store = nullptr;
 name const * g_string = nullptr;
 name const * g_string_empty = nullptr;
 name const * g_string_str = nullptr;
@@ -433,7 +399,6 @@ name const * g_psum = nullptr;
 name const * g_psum_cases_on = nullptr;
 name const * g_psum_inl = nullptr;
 name const * g_psum_inr = nullptr;
-name const * g_default_smt_config = nullptr;
 name const * g_smt_state_mk = nullptr;
 name const * g_smt_tactic_execute = nullptr;
 name const * g_smt_tactic_execute_with = nullptr;
@@ -450,9 +415,7 @@ name const * g_tactic_interactive_exact = nullptr;
 name const * g_trivial = nullptr;
 name const * g_thunk = nullptr;
 name const * g_to_fmt = nullptr;
-name const * g_to_int = nullptr;
 name const * g_to_string = nullptr;
-name const * g_to_real = nullptr;
 name const * g_trans_rel_left = nullptr;
 name const * g_trans_rel_right = nullptr;
 name const * g_true = nullptr;
@@ -494,7 +457,6 @@ void initialize_constants() {
     g_bool_ff = new name{"bool", "ff"};
     g_bool_tt = new name{"bool", "tt"};
     g_bind = new name{"bind"};
-    g_bv = new name{"bv"};
     g_caching_user_attribute = new name{"caching_user_attribute"};
     g_cast = new name{"cast"};
     g_cast_eq = new name{"cast_eq"};
@@ -515,13 +477,10 @@ void initialize_constants() {
     g_congr = new name{"congr"};
     g_congr_arg = new name{"congr_arg"};
     g_congr_fun = new name{"congr_fun"};
-    g_cyclic_numerals = new name{"cyclic_numerals"};
-    g_cyclic_numerals_bound = new name{"cyclic_numerals", "bound"};
     g_decidable = new name{"decidable"};
     g_decidable_by_contradiction = new name{"decidable", "by_contradiction"};
     g_decidable_to_bool = new name{"decidable", "to_bool"};
     g_discrete_field = new name{"discrete_field"};
-    g_distinct = new name{"distinct"};
     g_distrib = new name{"distrib"};
     g_dite = new name{"dite"};
     g_div = new name{"div"};
@@ -533,13 +492,9 @@ void initialize_constants() {
     g_eq = new name{"eq"};
     g_eq_cases_on = new name{"eq", "cases_on"};
     g_eq_drec = new name{"eq", "drec"};
-    g_eq_elim_inv_inv = new name{"eq", "elim_inv_inv"};
-    g_eq_intro = new name{"eq", "intro"};
     g_eq_mp = new name{"eq", "mp"};
     g_eq_mpr = new name{"eq", "mpr"};
-    g_eq_nrec = new name{"eq", "nrec"};
     g_eq_rec = new name{"eq", "rec"};
-    g_eq_rec_eq = new name{"eq_rec_eq"};
     g_eq_refl = new name{"eq", "refl"};
     g_eq_subst = new name{"eq", "subst"};
     g_eq_symm = new name{"eq", "symm"};
@@ -643,7 +598,7 @@ void initialize_constants() {
     g_int_ne_neg_of_pos = new name{"int", "ne_neg_of_pos"};
     g_int_neg_ne_zero_of_ne = new name{"int", "neg_ne_zero_of_ne"};
     g_int_zero_ne_neg_of_ne = new name{"int", "zero_ne_neg_of_ne"};
-    g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"};
+    g_int_decidable_linear_ordered_comm_group = new name{"int", "decidable_linear_ordered_comm_group"};
     g_interactive_parse = new name{"interactive", "parse"};
     g_inv = new name{"inv"};
     g_io = new name{"io"};
@@ -653,18 +608,11 @@ void initialize_constants() {
     g_is_associative_assoc = new name{"is_associative", "assoc"};
     g_is_commutative = new name{"is_commutative"};
     g_is_commutative_comm = new name{"is_commutative", "comm"};
-    g_is_int = new name{"is_int"};
-    g_is_trunc_is_prop = new name{"is_trunc", "is_prop"};
-    g_is_trunc_is_prop_elim = new name{"is_trunc", "is_prop", "elim"};
-    g_is_trunc_is_set = new name{"is_trunc", "is_set"};
     g_ite = new name{"ite"};
     g_left_distrib = new name{"left_distrib"};
     g_left_comm = new name{"left_comm"};
     g_le = new name{"le"};
-    g_le_refl = new name{"le", "refl"};
-    g_lift = new name{"lift"};
-    g_lift_down = new name{"lift", "down"};
-    g_lift_up = new name{"lift", "up"};
+    g_le_refl = new name{"le_refl"};
     g_linear_ordered_comm_ring = new name{"linear_ordered_comm_ring"};
     g_linear_ordered_ring = new name{"linear_ordered_ring"};
     g_linear_ordered_semiring = new name{"linear_ordered_semiring"};
@@ -672,11 +620,6 @@ void initialize_constants() {
     g_list_nil = new name{"list", "nil"};
     g_list_cons = new name{"list", "cons"};
     g_lt = new name{"lt"};
-    g_map = new name{"map"};
-    g_map_insert = new name{"map", "insert"};
-    g_map_lookup = new name{"map", "lookup"};
-    g_map_select = new name{"map", "select"};
-    g_map_store = new name{"map", "store"};
     g_match_failed = new name{"match_failed"};
     g_mod = new name{"mod"};
     g_monad = new name{"monad"};
@@ -702,7 +645,6 @@ void initialize_constants() {
     g_nat_has_mul = new name{"nat", "has_mul"};
     g_nat_has_div = new name{"nat", "has_div"};
     g_nat_has_sub = new name{"nat", "has_sub"};
-    g_nat_has_neg = new name{"nat", "has_neg"};
     g_nat_has_lt = new name{"nat", "has_lt"};
     g_nat_has_le = new name{"nat", "has_le"};
     g_nat_add = new name{"nat", "add"};
@@ -833,30 +775,23 @@ void initialize_constants() {
     g_to_pexpr = new name{"to_pexpr"};
     g_quot_mk = new name{"quot", "mk"};
     g_quot_lift = new name{"quot", "lift"};
-    g_rat_divide = new name{"rat", "divide"};
-    g_rat_of_num = new name{"rat", "of_num"};
-    g_rat_of_int = new name{"rat", "of_int"};
     g_real = new name{"real"};
-    g_real_has_zero = new name{"real", "has_zero"};
-    g_real_has_one = new name{"real", "has_one"};
+    g_real_of_int = new name{"real", "of_int"};
+    g_real_to_int = new name{"real", "to_int"};
+    g_real_is_int = new name{"real", "is_int"};
+    g_real_has_neg = new name{"real", "has_neg"};
+    g_real_has_div = new name{"real", "has_div"};
     g_real_has_add = new name{"real", "has_add"};
     g_real_has_mul = new name{"real", "has_mul"};
     g_real_has_sub = new name{"real", "has_sub"};
-    g_real_has_div = new name{"real", "has_div"};
-    g_real_has_le = new name{"real", "has_le"};
     g_real_has_lt = new name{"real", "has_lt"};
-    g_real_has_neg = new name{"real", "has_neg"};
-    g_real_is_int = new name{"real", "is_int"};
-    g_real_of_rat = new name{"real", "of_rat"};
-    g_real_of_int = new name{"real", "of_int"};
-    g_real_to_int = new name{"real", "to_int"};
+    g_real_has_le = new name{"real", "has_le"};
     g_rfl = new name{"rfl"};
     g_right_distrib = new name{"right_distrib"};
     g_ring = new name{"ring"};
     g_scope_trace = new name{"scope_trace"};
     g_set_of = new name{"set_of"};
     g_sep = new name{"sep"};
-    g_select = new name{"select"};
     g_semiring = new name{"semiring"};
     g_sigma = new name{"sigma"};
     g_sigma_cases_on = new name{"sigma", "cases_on"};
@@ -869,18 +804,12 @@ void initialize_constants() {
     g_psigma_fst = new name{"psigma", "fst"};
     g_psigma_snd = new name{"psigma", "snd"};
     g_simp = new name{"simp"};
-    g_simplifier_assoc_subst = new name{"simplifier", "assoc_subst"};
-    g_simplifier_congr_bin_op = new name{"simplifier", "congr_bin_op"};
-    g_simplifier_congr_bin_arg1 = new name{"simplifier", "congr_bin_arg1"};
-    g_simplifier_congr_bin_arg2 = new name{"simplifier", "congr_bin_arg2"};
-    g_simplifier_congr_bin_args = new name{"simplifier", "congr_bin_args"};
     g_singleton = new name{"singleton"};
     g_sizeof = new name{"sizeof"};
     g_smt_array = new name{"smt", "array"};
     g_smt_select = new name{"smt", "select"};
     g_smt_store = new name{"smt", "store"};
     g_smt_prove = new name{"smt", "prove"};
-    g_store = new name{"store"};
     g_string = new name{"string"};
     g_string_empty = new name{"string", "empty"};
     g_string_str = new name{"string", "str"};
@@ -904,7 +833,6 @@ void initialize_constants() {
     g_psum_cases_on = new name{"psum", "cases_on"};
     g_psum_inl = new name{"psum", "inl"};
     g_psum_inr = new name{"psum", "inr"};
-    g_default_smt_config = new name{"default_smt_config"};
     g_smt_state_mk = new name{"smt_state", "mk"};
     g_smt_tactic_execute = new name{"smt_tactic", "execute"};
     g_smt_tactic_execute_with = new name{"smt_tactic", "execute_with"};
@@ -921,9 +849,7 @@ void initialize_constants() {
     g_trivial = new name{"trivial"};
     g_thunk = new name{"thunk"};
     g_to_fmt = new name{"to_fmt"};
-    g_to_int = new name{"to_int"};
     g_to_string = new name{"to_string"};
-    g_to_real = new name{"to_real"};
     g_trans_rel_left = new name{"trans_rel_left"};
     g_trans_rel_right = new name{"trans_rel_right"};
     g_true = new name{"true"};
@@ -966,7 +892,6 @@ void finalize_constants() {
     delete g_bool_ff;
     delete g_bool_tt;
     delete g_bind;
-    delete g_bv;
     delete g_caching_user_attribute;
     delete g_cast;
     delete g_cast_eq;
@@ -987,13 +912,10 @@ void finalize_constants() {
     delete g_congr;
     delete g_congr_arg;
     delete g_congr_fun;
-    delete g_cyclic_numerals;
-    delete g_cyclic_numerals_bound;
     delete g_decidable;
     delete g_decidable_by_contradiction;
     delete g_decidable_to_bool;
     delete g_discrete_field;
-    delete g_distinct;
     delete g_distrib;
     delete g_dite;
     delete g_div;
@@ -1005,13 +927,9 @@ void finalize_constants() {
     delete g_eq;
     delete g_eq_cases_on;
     delete g_eq_drec;
-    delete g_eq_elim_inv_inv;
-    delete g_eq_intro;
     delete g_eq_mp;
     delete g_eq_mpr;
-    delete g_eq_nrec;
     delete g_eq_rec;
-    delete g_eq_rec_eq;
     delete g_eq_refl;
     delete g_eq_subst;
     delete g_eq_symm;
@@ -1125,18 +1043,11 @@ void finalize_constants() {
     delete g_is_associative_assoc;
     delete g_is_commutative;
     delete g_is_commutative_comm;
-    delete g_is_int;
-    delete g_is_trunc_is_prop;
-    delete g_is_trunc_is_prop_elim;
-    delete g_is_trunc_is_set;
     delete g_ite;
     delete g_left_distrib;
     delete g_left_comm;
     delete g_le;
     delete g_le_refl;
-    delete g_lift;
-    delete g_lift_down;
-    delete g_lift_up;
     delete g_linear_ordered_comm_ring;
     delete g_linear_ordered_ring;
     delete g_linear_ordered_semiring;
@@ -1144,11 +1055,6 @@ void finalize_constants() {
     delete g_list_nil;
     delete g_list_cons;
     delete g_lt;
-    delete g_map;
-    delete g_map_insert;
-    delete g_map_lookup;
-    delete g_map_select;
-    delete g_map_store;
     delete g_match_failed;
     delete g_mod;
     delete g_monad;
@@ -1174,7 +1080,6 @@ void finalize_constants() {
     delete g_nat_has_mul;
     delete g_nat_has_div;
     delete g_nat_has_sub;
-    delete g_nat_has_neg;
     delete g_nat_has_lt;
     delete g_nat_has_le;
     delete g_nat_add;
@@ -1305,30 +1210,23 @@ void finalize_constants() {
     delete g_to_pexpr;
     delete g_quot_mk;
     delete g_quot_lift;
-    delete g_rat_divide;
-    delete g_rat_of_num;
-    delete g_rat_of_int;
     delete g_real;
-    delete g_real_has_zero;
-    delete g_real_has_one;
+    delete g_real_of_int;
+    delete g_real_to_int;
+    delete g_real_is_int;
+    delete g_real_has_neg;
+    delete g_real_has_div;
     delete g_real_has_add;
     delete g_real_has_mul;
     delete g_real_has_sub;
-    delete g_real_has_div;
-    delete g_real_has_le;
     delete g_real_has_lt;
-    delete g_real_has_neg;
-    delete g_real_is_int;
-    delete g_real_of_rat;
-    delete g_real_of_int;
-    delete g_real_to_int;
+    delete g_real_has_le;
     delete g_rfl;
     delete g_right_distrib;
     delete g_ring;
     delete g_scope_trace;
     delete g_set_of;
     delete g_sep;
-    delete g_select;
     delete g_semiring;
     delete g_sigma;
     delete g_sigma_cases_on;
@@ -1341,18 +1239,12 @@ void finalize_constants() {
     delete g_psigma_fst;
     delete g_psigma_snd;
     delete g_simp;
-    delete g_simplifier_assoc_subst;
-    delete g_simplifier_congr_bin_op;
-    delete g_simplifier_congr_bin_arg1;
-    delete g_simplifier_congr_bin_arg2;
-    delete g_simplifier_congr_bin_args;
     delete g_singleton;
     delete g_sizeof;
     delete g_smt_array;
     delete g_smt_select;
     delete g_smt_store;
     delete g_smt_prove;
-    delete g_store;
     delete g_string;
     delete g_string_empty;
     delete g_string_str;
@@ -1376,7 +1268,6 @@ void finalize_constants() {
     delete g_psum_cases_on;
     delete g_psum_inl;
     delete g_psum_inr;
-    delete g_default_smt_config;
     delete g_smt_state_mk;
     delete g_smt_tactic_execute;
     delete g_smt_tactic_execute_with;
@@ -1393,9 +1284,7 @@ void finalize_constants() {
     delete g_trivial;
     delete g_thunk;
     delete g_to_fmt;
-    delete g_to_int;
     delete g_to_string;
-    delete g_to_real;
     delete g_trans_rel_left;
     delete g_trans_rel_right;
     delete g_true;
@@ -1437,7 +1326,6 @@ name const & get_bool_name() { return *g_bool; }
 name const & get_bool_ff_name() { return *g_bool_ff; }
 name const & get_bool_tt_name() { return *g_bool_tt; }
 name const & get_bind_name() { return *g_bind; }
-name const & get_bv_name() { return *g_bv; }
 name const & get_caching_user_attribute_name() { return *g_caching_user_attribute; }
 name const & get_cast_name() { return *g_cast; }
 name const & get_cast_eq_name() { return *g_cast_eq; }
@@ -1458,13 +1346,10 @@ name const & get_comm_semiring_name() { return *g_comm_semiring; }
 name const & get_congr_name() { return *g_congr; }
 name const & get_congr_arg_name() { return *g_congr_arg; }
 name const & get_congr_fun_name() { return *g_congr_fun; }
-name const & get_cyclic_numerals_name() { return *g_cyclic_numerals; }
-name const & get_cyclic_numerals_bound_name() { return *g_cyclic_numerals_bound; }
 name const & get_decidable_name() { return *g_decidable; }
 name const & get_decidable_by_contradiction_name() { return *g_decidable_by_contradiction; }
 name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; }
 name const & get_discrete_field_name() { return *g_discrete_field; }
-name const & get_distinct_name() { return *g_distinct; }
 name const & get_distrib_name() { return *g_distrib; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_div_name() { return *g_div; }
@@ -1476,13 +1361,9 @@ name const & get_Exists_name() { return *g_Exists; }
 name const & get_eq_name() { return *g_eq; }
 name const & get_eq_cases_on_name() { return *g_eq_cases_on; }
 name const & get_eq_drec_name() { return *g_eq_drec; }
-name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; }
-name const & get_eq_intro_name() { return *g_eq_intro; }
 name const & get_eq_mp_name() { return *g_eq_mp; }
 name const & get_eq_mpr_name() { return *g_eq_mpr; }
-name const & get_eq_nrec_name() { return *g_eq_nrec; }
 name const & get_eq_rec_name() { return *g_eq_rec; }
-name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }
 name const & get_eq_refl_name() { return *g_eq_refl; }
 name const & get_eq_subst_name() { return *g_eq_subst; }
 name const & get_eq_symm_name() { return *g_eq_symm; }
@@ -1596,18 +1477,11 @@ name const & get_is_associative_name() { return *g_is_associative; }
 name const & get_is_associative_assoc_name() { return *g_is_associative_assoc; }
 name const & get_is_commutative_name() { return *g_is_commutative; }
 name const & get_is_commutative_comm_name() { return *g_is_commutative_comm; }
-name const & get_is_int_name() { return *g_is_int; }
-name const & get_is_trunc_is_prop_name() { return *g_is_trunc_is_prop; }
-name const & get_is_trunc_is_prop_elim_name() { return *g_is_trunc_is_prop_elim; }
-name const & get_is_trunc_is_set_name() { return *g_is_trunc_is_set; }
 name const & get_ite_name() { return *g_ite; }
 name const & get_left_distrib_name() { return *g_left_distrib; }
 name const & get_left_comm_name() { return *g_left_comm; }
 name const & get_le_name() { return *g_le; }
 name const & get_le_refl_name() { return *g_le_refl; }
-name const & get_lift_name() { return *g_lift; }
-name const & get_lift_down_name() { return *g_lift_down; }
-name const & get_lift_up_name() { return *g_lift_up; }
 name const & get_linear_ordered_comm_ring_name() { return *g_linear_ordered_comm_ring; }
 name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; }
 name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; }
@@ -1615,11 +1489,6 @@ name const & get_list_name() { return *g_list; }
 name const & get_list_nil_name() { return *g_list_nil; }
 name const & get_list_cons_name() { return *g_list_cons; }
 name const & get_lt_name() { return *g_lt; }
-name const & get_map_name() { return *g_map; }
-name const & get_map_insert_name() { return *g_map_insert; }
-name const & get_map_lookup_name() { return *g_map_lookup; }
-name const & get_map_select_name() { return *g_map_select; }
-name const & get_map_store_name() { return *g_map_store; }
 name const & get_match_failed_name() { return *g_match_failed; }
 name const & get_mod_name() { return *g_mod; }
 name const & get_monad_name() { return *g_monad; }
@@ -1645,7 +1514,6 @@ name const & get_nat_has_add_name() { return *g_nat_has_add; }
 name const & get_nat_has_mul_name() { return *g_nat_has_mul; }
 name const & get_nat_has_div_name() { return *g_nat_has_div; }
 name const & get_nat_has_sub_name() { return *g_nat_has_sub; }
-name const & get_nat_has_neg_name() { return *g_nat_has_neg; }
 name const & get_nat_has_lt_name() { return *g_nat_has_lt; }
 name const & get_nat_has_le_name() { return *g_nat_has_le; }
 name const & get_nat_add_name() { return *g_nat_add; }
@@ -1776,30 +1644,23 @@ name const & get_put_nat_name() { return *g_put_nat; }
 name const & get_to_pexpr_name() { return *g_to_pexpr; }
 name const & get_quot_mk_name() { return *g_quot_mk; }
 name const & get_quot_lift_name() { return *g_quot_lift; }
-name const & get_rat_divide_name() { return *g_rat_divide; }
-name const & get_rat_of_num_name() { return *g_rat_of_num; }
-name const & get_rat_of_int_name() { return *g_rat_of_int; }
 name const & get_real_name() { return *g_real; }
-name const & get_real_has_zero_name() { return *g_real_has_zero; }
-name const & get_real_has_one_name() { return *g_real_has_one; }
+name const & get_real_of_int_name() { return *g_real_of_int; }
+name const & get_real_to_int_name() { return *g_real_to_int; }
+name const & get_real_is_int_name() { return *g_real_is_int; }
+name const & get_real_has_neg_name() { return *g_real_has_neg; }
+name const & get_real_has_div_name() { return *g_real_has_div; }
 name const & get_real_has_add_name() { return *g_real_has_add; }
 name const & get_real_has_mul_name() { return *g_real_has_mul; }
 name const & get_real_has_sub_name() { return *g_real_has_sub; }
-name const & get_real_has_div_name() { return *g_real_has_div; }
-name const & get_real_has_le_name() { return *g_real_has_le; }
 name const & get_real_has_lt_name() { return *g_real_has_lt; }
-name const & get_real_has_neg_name() { return *g_real_has_neg; }
-name const & get_real_is_int_name() { return *g_real_is_int; }
-name const & get_real_of_rat_name() { return *g_real_of_rat; }
-name const & get_real_of_int_name() { return *g_real_of_int; }
-name const & get_real_to_int_name() { return *g_real_to_int; }
+name const & get_real_has_le_name() { return *g_real_has_le; }
 name const & get_rfl_name() { return *g_rfl; }
 name const & get_right_distrib_name() { return *g_right_distrib; }
 name const & get_ring_name() { return *g_ring; }
 name const & get_scope_trace_name() { return *g_scope_trace; }
 name const & get_set_of_name() { return *g_set_of; }
 name const & get_sep_name() { return *g_sep; }
-name const & get_select_name() { return *g_select; }
 name const & get_semiring_name() { return *g_semiring; }
 name const & get_sigma_name() { return *g_sigma; }
 name const & get_sigma_cases_on_name() { return *g_sigma_cases_on; }
@@ -1812,18 +1673,12 @@ name const & get_psigma_mk_name() { return *g_psigma_mk; }
 name const & get_psigma_fst_name() { return *g_psigma_fst; }
 name const & get_psigma_snd_name() { return *g_psigma_snd; }
 name const & get_simp_name() { return *g_simp; }
-name const & get_simplifier_assoc_subst_name() { return *g_simplifier_assoc_subst; }
-name const & get_simplifier_congr_bin_op_name() { return *g_simplifier_congr_bin_op; }
-name const & get_simplifier_congr_bin_arg1_name() { return *g_simplifier_congr_bin_arg1; }
-name const & get_simplifier_congr_bin_arg2_name() { return *g_simplifier_congr_bin_arg2; }
-name const & get_simplifier_congr_bin_args_name() { return *g_simplifier_congr_bin_args; }
 name const & get_singleton_name() { return *g_singleton; }
 name const & get_sizeof_name() { return *g_sizeof; }
 name const & get_smt_array_name() { return *g_smt_array; }
 name const & get_smt_select_name() { return *g_smt_select; }
 name const & get_smt_store_name() { return *g_smt_store; }
 name const & get_smt_prove_name() { return *g_smt_prove; }
-name const & get_store_name() { return *g_store; }
 name const & get_string_name() { return *g_string; }
 name const & get_string_empty_name() { return *g_string_empty; }
 name const & get_string_str_name() { return *g_string_str; }
@@ -1847,7 +1702,6 @@ name const & get_psum_name() { return *g_psum; }
 name const & get_psum_cases_on_name() { return *g_psum_cases_on; }
 name const & get_psum_inl_name() { return *g_psum_inl; }
 name const & get_psum_inr_name() { return *g_psum_inr; }
-name const & get_default_smt_config_name() { return *g_default_smt_config; }
 name const & get_smt_state_mk_name() { return *g_smt_state_mk; }
 name const & get_smt_tactic_execute_name() { return *g_smt_tactic_execute; }
 name const & get_smt_tactic_execute_with_name() { return *g_smt_tactic_execute_with; }
@@ -1864,9 +1718,7 @@ name const & get_tactic_interactive_exact_name() { return *g_tactic_interactive_
 name const & get_trivial_name() { return *g_trivial; }
 name const & get_thunk_name() { return *g_thunk; }
 name const & get_to_fmt_name() { return *g_to_fmt; }
-name const & get_to_int_name() { return *g_to_int; }
 name const & get_to_string_name() { return *g_to_string; }
-name const & get_to_real_name() { return *g_to_real; }
 name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
 name const & get_trans_rel_right_name() { return *g_trans_rel_right; }
 name const & get_true_name() { return *g_true; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 492c3b4043..360d7680d5 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -25,7 +25,6 @@ name const & get_bool_name();
 name const & get_bool_ff_name();
 name const & get_bool_tt_name();
 name const & get_bind_name();
-name const & get_bv_name();
 name const & get_caching_user_attribute_name();
 name const & get_cast_name();
 name const & get_cast_eq_name();
@@ -46,13 +45,10 @@ name const & get_comm_semiring_name();
 name const & get_congr_name();
 name const & get_congr_arg_name();
 name const & get_congr_fun_name();
-name const & get_cyclic_numerals_name();
-name const & get_cyclic_numerals_bound_name();
 name const & get_decidable_name();
 name const & get_decidable_by_contradiction_name();
 name const & get_decidable_to_bool_name();
 name const & get_discrete_field_name();
-name const & get_distinct_name();
 name const & get_distrib_name();
 name const & get_dite_name();
 name const & get_div_name();
@@ -64,13 +60,9 @@ name const & get_Exists_name();
 name const & get_eq_name();
 name const & get_eq_cases_on_name();
 name const & get_eq_drec_name();
-name const & get_eq_elim_inv_inv_name();
-name const & get_eq_intro_name();
 name const & get_eq_mp_name();
 name const & get_eq_mpr_name();
-name const & get_eq_nrec_name();
 name const & get_eq_rec_name();
-name const & get_eq_rec_eq_name();
 name const & get_eq_refl_name();
 name const & get_eq_subst_name();
 name const & get_eq_symm_name();
@@ -184,18 +176,11 @@ name const & get_is_associative_name();
 name const & get_is_associative_assoc_name();
 name const & get_is_commutative_name();
 name const & get_is_commutative_comm_name();
-name const & get_is_int_name();
-name const & get_is_trunc_is_prop_name();
-name const & get_is_trunc_is_prop_elim_name();
-name const & get_is_trunc_is_set_name();
 name const & get_ite_name();
 name const & get_left_distrib_name();
 name const & get_left_comm_name();
 name const & get_le_name();
 name const & get_le_refl_name();
-name const & get_lift_name();
-name const & get_lift_down_name();
-name const & get_lift_up_name();
 name const & get_linear_ordered_comm_ring_name();
 name const & get_linear_ordered_ring_name();
 name const & get_linear_ordered_semiring_name();
@@ -203,11 +188,6 @@ name const & get_list_name();
 name const & get_list_nil_name();
 name const & get_list_cons_name();
 name const & get_lt_name();
-name const & get_map_name();
-name const & get_map_insert_name();
-name const & get_map_lookup_name();
-name const & get_map_select_name();
-name const & get_map_store_name();
 name const & get_match_failed_name();
 name const & get_mod_name();
 name const & get_monad_name();
@@ -233,7 +213,6 @@ name const & get_nat_has_add_name();
 name const & get_nat_has_mul_name();
 name const & get_nat_has_div_name();
 name const & get_nat_has_sub_name();
-name const & get_nat_has_neg_name();
 name const & get_nat_has_lt_name();
 name const & get_nat_has_le_name();
 name const & get_nat_add_name();
@@ -364,30 +343,23 @@ name const & get_put_nat_name();
 name const & get_to_pexpr_name();
 name const & get_quot_mk_name();
 name const & get_quot_lift_name();
-name const & get_rat_divide_name();
-name const & get_rat_of_num_name();
-name const & get_rat_of_int_name();
 name const & get_real_name();
-name const & get_real_has_zero_name();
-name const & get_real_has_one_name();
+name const & get_real_of_int_name();
+name const & get_real_to_int_name();
+name const & get_real_is_int_name();
+name const & get_real_has_neg_name();
+name const & get_real_has_div_name();
 name const & get_real_has_add_name();
 name const & get_real_has_mul_name();
 name const & get_real_has_sub_name();
-name const & get_real_has_div_name();
-name const & get_real_has_le_name();
 name const & get_real_has_lt_name();
-name const & get_real_has_neg_name();
-name const & get_real_is_int_name();
-name const & get_real_of_rat_name();
-name const & get_real_of_int_name();
-name const & get_real_to_int_name();
+name const & get_real_has_le_name();
 name const & get_rfl_name();
 name const & get_right_distrib_name();
 name const & get_ring_name();
 name const & get_scope_trace_name();
 name const & get_set_of_name();
 name const & get_sep_name();
-name const & get_select_name();
 name const & get_semiring_name();
 name const & get_sigma_name();
 name const & get_sigma_cases_on_name();
@@ -400,18 +372,12 @@ name const & get_psigma_mk_name();
 name const & get_psigma_fst_name();
 name const & get_psigma_snd_name();
 name const & get_simp_name();
-name const & get_simplifier_assoc_subst_name();
-name const & get_simplifier_congr_bin_op_name();
-name const & get_simplifier_congr_bin_arg1_name();
-name const & get_simplifier_congr_bin_arg2_name();
-name const & get_simplifier_congr_bin_args_name();
 name const & get_singleton_name();
 name const & get_sizeof_name();
 name const & get_smt_array_name();
 name const & get_smt_select_name();
 name const & get_smt_store_name();
 name const & get_smt_prove_name();
-name const & get_store_name();
 name const & get_string_name();
 name const & get_string_empty_name();
 name const & get_string_str_name();
@@ -435,7 +401,6 @@ name const & get_psum_name();
 name const & get_psum_cases_on_name();
 name const & get_psum_inl_name();
 name const & get_psum_inr_name();
-name const & get_default_smt_config_name();
 name const & get_smt_state_mk_name();
 name const & get_smt_tactic_execute_name();
 name const & get_smt_tactic_execute_with_name();
@@ -452,9 +417,7 @@ name const & get_tactic_interactive_exact_name();
 name const & get_trivial_name();
 name const & get_thunk_name();
 name const & get_to_fmt_name();
-name const & get_to_int_name();
 name const & get_to_string_name();
-name const & get_to_real_name();
 name const & get_trans_rel_left_name();
 name const & get_trans_rel_right_name();
 name const & get_true_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 239b000f35..acc9fc780b 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -18,7 +18,6 @@ bool
 bool.ff
 bool.tt
 bind
-bv
 caching_user_attribute
 cast
 cast_eq
@@ -39,13 +38,10 @@ comm_semiring
 congr
 congr_arg
 congr_fun
-cyclic_numerals
-cyclic_numerals.bound
 decidable
 decidable.by_contradiction
 decidable.to_bool
 discrete_field
-distinct
 distrib
 dite
 div
@@ -57,13 +53,9 @@ Exists
 eq
 eq.cases_on
 eq.drec
-eq.elim_inv_inv
-eq.intro
 eq.mp
 eq.mpr
-eq.nrec
 eq.rec
-eq_rec_eq
 eq.refl
 eq.subst
 eq.symm
@@ -167,7 +159,7 @@ int.neg_ne_of_pos
 int.ne_neg_of_pos
 int.neg_ne_zero_of_ne
 int.zero_ne_neg_of_ne
-int_decidable_linear_ordered_comm_group
+int.decidable_linear_ordered_comm_group
 interactive.parse
 inv
 io
@@ -177,18 +169,11 @@ is_associative
 is_associative.assoc
 is_commutative
 is_commutative.comm
-is_int
-is_trunc.is_prop
-is_trunc.is_prop.elim
-is_trunc.is_set
 ite
 left_distrib
 left_comm
 le
-le.refl
-lift
-lift.down
-lift.up
+le_refl
 linear_ordered_comm_ring
 linear_ordered_ring
 linear_ordered_semiring
@@ -196,11 +181,6 @@ list
 list.nil
 list.cons
 lt
-map
-map.insert
-map.lookup
-map.select
-map.store
 match_failed
 mod
 monad
@@ -226,7 +206,6 @@ nat.has_add
 nat.has_mul
 nat.has_div
 nat.has_sub
-nat.has_neg
 nat.has_lt
 nat.has_le
 nat.add
@@ -357,30 +336,23 @@ put_nat
 to_pexpr
 quot.mk
 quot.lift
-rat.divide
-rat.of_num
-rat.of_int
 real
-real.has_zero
-real.has_one
+real.of_int
+real.to_int
+real.is_int
+real.has_neg
+real.has_div
 real.has_add
 real.has_mul
 real.has_sub
-real.has_div
-real.has_le
 real.has_lt
-real.has_neg
-real.is_int
-real.of_rat
-real.of_int
-real.to_int
+real.has_le
 rfl
 right_distrib
 ring
 scope_trace
 set_of
 sep
-select
 semiring
 sigma
 sigma.cases_on
@@ -393,18 +365,12 @@ psigma.mk
 psigma.fst
 psigma.snd
 simp
-simplifier.assoc_subst
-simplifier.congr_bin_op
-simplifier.congr_bin_arg1
-simplifier.congr_bin_arg2
-simplifier.congr_bin_args
 singleton
 sizeof
 smt.array
 smt.select
 smt.store
 smt.prove
-store
 string
 string.empty
 string.str
@@ -428,7 +394,6 @@ psum
 psum.cases_on
 psum.inl
 psum.inr
-default_smt_config
 smt_state.mk
 smt_tactic.execute
 smt_tactic.execute_with
@@ -445,9 +410,7 @@ tactic.interactive.exact
 trivial
 thunk
 to_fmt
-to_int
 to_string
-to_real
 trans_rel_left
 trans_rel_right
 true
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 051b4f2064..257b22d1a0 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -65,6 +65,10 @@ name_set get_opened_namespaces(environment const & env) {
     return get_extension(env).m_opened_namespaces;
 }
 
+bool is_namespace(environment const & env, name const & n) {
+    return get_extension(env).m_namespace_set.contains(n);
+}
+
 optional<name> to_valid_namespace_name(environment const & env, name const & n) {
     scope_mng_ext const & ext = get_extension(env);
     if (ext.m_namespace_set.contains(n))
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index d95ae5ff96..5675dcd947 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -67,6 +67,9 @@ environment mark_namespace_as_open(environment const & env, name const & n);
 /** \brief Return the set of namespaces marked as "open" using \c mark_namespace_as_open. */
 name_set get_opened_namespaces(environment const & env);
 
+/** \brief Return true iff \c n is a namespace */
+bool is_namespace(environment const & env, name const & n);
+
 /** \brief Auxilary template used to simplify the creation of environment extensions that support
     the scope */
 template<typename Config>
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index b9f42c4d0f..05f8cd3c78 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -186,7 +186,7 @@ expr simplify_core_fn::remove_unnecessary_casts(expr const & e) {
                 buffer<expr> cast_args;
                 expr f_cast = get_app_args(args[i], cast_args);
                 name n_f = const_name(f_cast);
-                if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) {
+                if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name()) {
                     lean_assert(cast_args.size() == 6);
                     expr major_premise = cast_args[5];
                     expr f_major_premise = get_app_fn(major_premise);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index b34338b15c..3cc01552ca 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -155,10 +155,6 @@ bool has_pprod_decls(environment const & env) {
     return has_constructor(env, get_pprod_mk_name(), get_pprod_name(), 4);
 }
 
-bool has_lift_decls(environment const & env) {
-    return has_constructor(env, get_lift_up_name(), get_lift_name(), 2);
-}
-
 /* n is considered to be recursive if it is an inductive datatype and
    1) It has a constructor that takes n as an argument
    2) It is part of a mutually recursive declaration, and some constructor
diff --git a/src/library/util.h b/src/library/util.h
index 9203a97e9e..e602641beb 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -48,7 +48,6 @@ bool has_punit_decls(environment const & env);
 bool has_pprod_decls(environment const & env);
 bool has_eq_decls(environment const & env);
 bool has_heq_decls(environment const & env);
-bool has_lift_decls(environment const & env);
 
 /** \brief Return true iff \c n is the name of a recursive datatype in \c env.
     That is, it must be an inductive datatype AND contain a recursive constructor.
diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp
index 65e89f4711..e6cc14dd92 100644
--- a/src/library/vm/vm_environment.cpp
+++ b/src/library/vm/vm_environment.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/inductive/inductive.h"
 #include "kernel/standard_kernel.h"
 #include "library/module.h"
+#include "library/scoped_ext.h"
 #include "library/projection.h"
 #include "library/util.h"
 #include "library/relation_manager.h"
@@ -210,6 +211,10 @@ vm_obj environment_decl_pos_info(vm_obj const & env, vm_obj const & n) {
     }
 }
 
+vm_obj environment_is_namespace(vm_obj const & env, vm_obj const & n) {
+    return mk_vm_bool(is_namespace(to_env(env), to_name(n)));
+}
+
 /*
 structure projection_info :=
 (cname : name)
@@ -247,6 +252,7 @@ void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "inductive_num_params"}),  environment_inductive_num_params);
     DECLARE_VM_BUILTIN(name({"environment", "inductive_num_indices"}), environment_inductive_num_indices);
     DECLARE_VM_BUILTIN(name({"environment", "inductive_dep_elim"}),    environment_inductive_dep_elim);
+    DECLARE_VM_BUILTIN(name({"environment", "is_namespace"}),          environment_is_namespace);
     DECLARE_VM_BUILTIN(name({"environment", "is_ginductive"}),         environment_is_ginductive);
     DECLARE_VM_BUILTIN(name({"environment", "is_projection"}),         environment_is_projection);
     DECLARE_VM_BUILTIN(name({"environment", "relation_info"}),         environment_relation_info);
diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean
new file mode 100644
index 0000000000..a867d7f6b2
--- /dev/null
+++ b/tests/lean/run/check_constants.lean
@@ -0,0 +1,438 @@
+-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py
+import smt system.io
+open tactic
+meta def script_check_id (n : name) : tactic unit :=
+do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail ("identifier '" ++ to_string n ++ "' is not a constant, namespace nor attribute")
+run_command script_check_id `abs
+run_command script_check_id `absurd
+run_command script_check_id `acc.cases_on
+run_command script_check_id `add
+run_command script_check_id `add_comm_group
+run_command script_check_id `add_comm_semigroup
+run_command script_check_id `add_group
+run_command script_check_id `add_monoid
+run_command script_check_id `and
+run_command script_check_id `and.elim_left
+run_command script_check_id `and.elim_right
+run_command script_check_id `and.intro
+run_command script_check_id `andthen
+run_command script_check_id `auto_param
+run_command script_check_id `bit0
+run_command script_check_id `bit1
+run_command script_check_id `bool
+run_command script_check_id `bool.ff
+run_command script_check_id `bool.tt
+run_command script_check_id `bind
+run_command script_check_id `caching_user_attribute
+run_command script_check_id `cast
+run_command script_check_id `cast_eq
+run_command script_check_id `cast_heq
+run_command script_check_id `char
+run_command script_check_id `char.of_nat
+run_command script_check_id `char.of_nat_ne_of_ne
+run_command script_check_id `classical
+run_command script_check_id `classical.prop_decidable
+run_command script_check_id `classical.type_decidable_eq
+run_command script_check_id `coe
+run_command script_check_id `coe_fn
+run_command script_check_id `coe_sort
+run_command script_check_id `coe_to_lift
+run_command script_check_id `combinator.K
+run_command script_check_id `comm_ring
+run_command script_check_id `comm_semiring
+run_command script_check_id `congr
+run_command script_check_id `congr_arg
+run_command script_check_id `congr_fun
+run_command script_check_id `decidable
+run_command script_check_id `decidable.by_contradiction
+run_command script_check_id `decidable.to_bool
+run_command script_check_id `discrete_field
+run_command script_check_id `distrib
+run_command script_check_id `dite
+run_command script_check_id `div
+run_command script_check_id `id
+run_command script_check_id `empty
+run_command script_check_id `empty.rec
+run_command script_check_id `emptyc
+run_command script_check_id `Exists
+run_command script_check_id `eq
+run_command script_check_id `eq.cases_on
+run_command script_check_id `eq.drec
+run_command script_check_id `eq.mp
+run_command script_check_id `eq.mpr
+run_command script_check_id `eq.rec
+run_command script_check_id `eq.refl
+run_command script_check_id `eq.subst
+run_command script_check_id `eq.symm
+run_command script_check_id `eq.trans
+run_command script_check_id `eq_of_heq
+run_command script_check_id `eq_rec_heq
+run_command script_check_id `eq_true_intro
+run_command script_check_id `eq_false_intro
+run_command script_check_id `eq_self_iff_true
+run_command script_check_id `exists.elim
+run_command script_check_id `format
+run_command script_check_id `functor
+run_command script_check_id `false
+run_command script_check_id `false_of_true_iff_false
+run_command script_check_id `false_of_true_eq_false
+run_command script_check_id `true_eq_false_of_false
+run_command script_check_id `false.rec
+run_command script_check_id `field
+run_command script_check_id `fin
+run_command script_check_id `fin.mk
+run_command script_check_id `fin.ne_of_vne
+run_command script_check_id `forall_congr
+run_command script_check_id `forall_congr_eq
+run_command script_check_id `forall_not_of_not_exists
+run_command script_check_id `funext
+run_command script_check_id `ge
+run_command script_check_id `get_line
+run_command script_check_id `gt
+run_command script_check_id `has_add
+run_command script_check_id `has_div
+run_command script_check_id `has_mul
+run_command script_check_id `has_inv
+run_command script_check_id `has_le
+run_command script_check_id `has_lt
+run_command script_check_id `has_neg
+run_command script_check_id `has_one
+run_command script_check_id `has_one.one
+run_command script_check_id `has_sizeof
+run_command script_check_id `has_sizeof.mk
+run_command script_check_id `has_sizeof.sizeof
+run_command script_check_id `has_sub
+run_command script_check_id `has_to_format
+run_command script_check_id `has_to_string
+run_command script_check_id `has_zero
+run_command script_check_id `has_zero.zero
+run_command script_check_id `has_coe_t
+run_command script_check_id `heq
+run_command script_check_id `heq.refl
+run_command script_check_id `heq.symm
+run_command script_check_id `heq.trans
+run_command script_check_id `heq_of_eq
+run_command script_check_id `id_locked
+run_command script_check_id `if_neg
+run_command script_check_id `if_pos
+run_command script_check_id `iff
+run_command script_check_id `iff.elim_left
+run_command script_check_id `iff.elim_right
+run_command script_check_id `iff_false_intro
+run_command script_check_id `iff.intro
+run_command script_check_id `iff.mp
+run_command script_check_id `iff.mpr
+run_command script_check_id `iff.refl
+run_command script_check_id `iff.symm
+run_command script_check_id `iff.trans
+run_command script_check_id `iff_true_intro
+run_command script_check_id `imp_congr
+run_command script_check_id `imp_congr_eq
+run_command script_check_id `imp_congr_ctx
+run_command script_check_id `imp_congr_ctx_eq
+run_command script_check_id `implies
+run_command script_check_id `implies_of_if_neg
+run_command script_check_id `implies_of_if_pos
+run_command script_check_id `implies.resolve
+run_command script_check_id `insert
+run_command script_check_id `int
+run_command script_check_id `int.of_nat
+run_command script_check_id `int.has_zero
+run_command script_check_id `int.has_one
+run_command script_check_id `int.has_add
+run_command script_check_id `int.has_mul
+run_command script_check_id `int.has_sub
+run_command script_check_id `int.has_div
+run_command script_check_id `int.has_le
+run_command script_check_id `int.has_lt
+run_command script_check_id `int.has_neg
+run_command script_check_id `int.has_mod
+run_command script_check_id `int.bit0_nonneg
+run_command script_check_id `int.bit1_nonneg
+run_command script_check_id `int.one_nonneg
+run_command script_check_id `int.zero_nonneg
+run_command script_check_id `int.bit0_pos
+run_command script_check_id `int.bit1_pos
+run_command script_check_id `int.one_pos
+run_command script_check_id `int.nat_abs_zero
+run_command script_check_id `int.nat_abs_one
+run_command script_check_id `int.nat_abs_bit0_step
+run_command script_check_id `int.nat_abs_bit1_nonneg_step
+run_command script_check_id `int.ne_of_nat_ne_nonneg_case
+run_command script_check_id `int.ne_neg_of_ne
+run_command script_check_id `int.neg_ne_of_pos
+run_command script_check_id `int.ne_neg_of_pos
+run_command script_check_id `int.neg_ne_zero_of_ne
+run_command script_check_id `int.zero_ne_neg_of_ne
+run_command script_check_id `int.decidable_linear_ordered_comm_group
+run_command script_check_id `interactive.parse
+run_command script_check_id `inv
+run_command script_check_id `io
+run_command script_check_id `io.functor
+run_command script_check_id `io.monad
+run_command script_check_id `is_associative
+run_command script_check_id `is_associative.assoc
+run_command script_check_id `is_commutative
+run_command script_check_id `is_commutative.comm
+run_command script_check_id `ite
+run_command script_check_id `left_distrib
+run_command script_check_id `left_comm
+run_command script_check_id `le
+run_command script_check_id `le_refl
+run_command script_check_id `linear_ordered_comm_ring
+run_command script_check_id `linear_ordered_ring
+run_command script_check_id `linear_ordered_semiring
+run_command script_check_id `list
+run_command script_check_id `list.nil
+run_command script_check_id `list.cons
+run_command script_check_id `lt
+run_command script_check_id `match_failed
+run_command script_check_id `mod
+run_command script_check_id `monad
+run_command script_check_id `monad.map
+run_command script_check_id `monad.bind
+run_command script_check_id `monad.ret
+run_command script_check_id `monad_fail
+run_command script_check_id `monoid
+run_command script_check_id `mul
+run_command script_check_id `mul_one
+run_command script_check_id `mul_zero
+run_command script_check_id `mul_zero_class
+run_command script_check_id `name
+run_command script_check_id `name.anonymous
+run_command script_check_id `name.mk_string
+run_command script_check_id `nat
+run_command script_check_id `nat.of_num
+run_command script_check_id `nat.succ
+run_command script_check_id `nat.zero
+run_command script_check_id `nat.has_zero
+run_command script_check_id `nat.has_one
+run_command script_check_id `nat.has_add
+run_command script_check_id `nat.has_mul
+run_command script_check_id `nat.has_div
+run_command script_check_id `nat.has_sub
+run_command script_check_id `nat.has_lt
+run_command script_check_id `nat.has_le
+run_command script_check_id `nat.add
+run_command script_check_id `nat.no_confusion
+run_command script_check_id `nat.cases_on
+run_command script_check_id `nat.bit0_ne
+run_command script_check_id `nat.bit0_ne_bit1
+run_command script_check_id `nat.bit0_ne_zero
+run_command script_check_id `nat.bit0_ne_one
+run_command script_check_id `nat.bit1_ne
+run_command script_check_id `nat.bit1_ne_bit0
+run_command script_check_id `nat.bit1_ne_zero
+run_command script_check_id `nat.bit1_ne_one
+run_command script_check_id `nat.zero_ne_one
+run_command script_check_id `nat.zero_ne_bit0
+run_command script_check_id `nat.zero_ne_bit1
+run_command script_check_id `nat.one_ne_zero
+run_command script_check_id `nat.one_ne_bit0
+run_command script_check_id `nat.one_ne_bit1
+run_command script_check_id `nat.bit0_lt
+run_command script_check_id `nat.bit1_lt
+run_command script_check_id `nat.bit0_lt_bit1
+run_command script_check_id `nat.bit1_lt_bit0
+run_command script_check_id `nat.zero_lt_one
+run_command script_check_id `nat.zero_lt_bit1
+run_command script_check_id `nat.zero_lt_bit0
+run_command script_check_id `nat.one_lt_bit0
+run_command script_check_id `nat.one_lt_bit1
+run_command script_check_id `nat.le_of_lt
+run_command script_check_id `nat.le_refl
+run_command script_check_id `ne
+run_command script_check_id `neg
+run_command script_check_id `neq_of_not_iff
+run_command script_check_id `norm_num.add1
+run_command script_check_id `norm_num.add1_bit0
+run_command script_check_id `norm_num.add1_bit1_helper
+run_command script_check_id `norm_num.add1_one
+run_command script_check_id `norm_num.add1_zero
+run_command script_check_id `norm_num.add_div_helper
+run_command script_check_id `norm_num.bin_add_zero
+run_command script_check_id `norm_num.bin_zero_add
+run_command script_check_id `norm_num.bit0_add_bit0_helper
+run_command script_check_id `norm_num.bit0_add_bit1_helper
+run_command script_check_id `norm_num.bit0_add_one
+run_command script_check_id `norm_num.bit1_add_bit0_helper
+run_command script_check_id `norm_num.bit1_add_bit1_helper
+run_command script_check_id `norm_num.bit1_add_one_helper
+run_command script_check_id `norm_num.div_add_helper
+run_command script_check_id `norm_num.div_eq_div_helper
+run_command script_check_id `norm_num.div_helper
+run_command script_check_id `norm_num.div_mul_helper
+run_command script_check_id `norm_num.mk_cong
+run_command script_check_id `norm_num.mul_bit0_helper
+run_command script_check_id `norm_num.mul_bit1_helper
+run_command script_check_id `norm_num.mul_div_helper
+run_command script_check_id `norm_num.neg_add_neg_helper
+run_command script_check_id `norm_num.neg_add_pos_helper1
+run_command script_check_id `norm_num.neg_add_pos_helper2
+run_command script_check_id `norm_num.neg_mul_neg_helper
+run_command script_check_id `norm_num.neg_mul_pos_helper
+run_command script_check_id `norm_num.neg_neg_helper
+run_command script_check_id `norm_num.neg_zero_helper
+run_command script_check_id `norm_num.nonneg_bit0_helper
+run_command script_check_id `norm_num.nonneg_bit1_helper
+run_command script_check_id `norm_num.nonzero_of_div_helper
+run_command script_check_id `norm_num.nonzero_of_neg_helper
+run_command script_check_id `norm_num.nonzero_of_pos_helper
+run_command script_check_id `norm_num.one_add_bit0
+run_command script_check_id `norm_num.one_add_bit1_helper
+run_command script_check_id `norm_num.one_add_one
+run_command script_check_id `norm_num.pos_add_neg_helper
+run_command script_check_id `norm_num.pos_add_pos_helper
+run_command script_check_id `norm_num.pos_bit0_helper
+run_command script_check_id `norm_num.pos_bit1_helper
+run_command script_check_id `norm_num.pos_mul_neg_helper
+run_command script_check_id `norm_num.sub_eq_add_neg_helper
+run_command script_check_id `norm_num.sub_nat_zero_helper
+run_command script_check_id `norm_num.sub_nat_pos_helper
+run_command script_check_id `norm_num.subst_into_div
+run_command script_check_id `norm_num.subst_into_prod
+run_command script_check_id `norm_num.subst_into_subtr
+run_command script_check_id `norm_num.subst_into_sum
+run_command script_check_id `not
+run_command script_check_id `not_of_iff_false
+run_command script_check_id `not_of_eq_false
+run_command script_check_id `not_of_not_not_not
+run_command script_check_id `num
+run_command script_check_id `num.pos
+run_command script_check_id `num.zero
+run_command script_check_id `of_eq_true
+run_command script_check_id `of_iff_true
+run_command script_check_id `one
+run_command script_check_id `one_mul
+run_command script_check_id `option
+run_command script_check_id `option.none
+run_command script_check_id `option.some
+run_command script_check_id `opt_param
+run_command script_check_id `or
+run_command script_check_id `or.elim
+run_command script_check_id `or.intro_left
+run_command script_check_id `or.intro_right
+run_command script_check_id `or.neg_resolve_left
+run_command script_check_id `or.neg_resolve_right
+run_command script_check_id `or.rec
+run_command script_check_id `or.resolve_left
+run_command script_check_id `or.resolve_right
+run_command script_check_id `orelse
+run_command script_check_id `out_param
+run_command script_check_id `punit
+run_command script_check_id `punit.star
+run_command script_check_id `pos_num
+run_command script_check_id `pos_num.bit0
+run_command script_check_id `pos_num.bit1
+run_command script_check_id `pos_num.one
+run_command script_check_id `prod.mk
+run_command script_check_id `pprod
+run_command script_check_id `pprod.mk
+run_command script_check_id `pprod.fst
+run_command script_check_id `pprod.snd
+run_command script_check_id `propext
+run_command script_check_id `pexpr
+run_command script_check_id `pexpr.subst
+run_command script_check_id `pre_monad.bind
+run_command script_check_id `pre_monad.and_then
+run_command script_check_id `pre_monad.seq
+run_command script_check_id `put_str
+run_command script_check_id `put_nat
+run_command script_check_id `to_pexpr
+run_command script_check_id `quot.mk
+run_command script_check_id `quot.lift
+run_command script_check_id `real
+run_command script_check_id `real.of_int
+run_command script_check_id `real.to_int
+run_command script_check_id `real.is_int
+run_command script_check_id `real.has_neg
+run_command script_check_id `real.has_div
+run_command script_check_id `real.has_add
+run_command script_check_id `real.has_mul
+run_command script_check_id `real.has_sub
+run_command script_check_id `real.has_lt
+run_command script_check_id `real.has_le
+run_command script_check_id `rfl
+run_command script_check_id `right_distrib
+run_command script_check_id `ring
+run_command script_check_id `scope_trace
+run_command script_check_id `set_of
+run_command script_check_id `sep
+run_command script_check_id `semiring
+run_command script_check_id `sigma
+run_command script_check_id `sigma.cases_on
+run_command script_check_id `sigma.mk
+run_command script_check_id `sigma.fst
+run_command script_check_id `sigma.snd
+run_command script_check_id `psigma
+run_command script_check_id `psigma.cases_on
+run_command script_check_id `psigma.mk
+run_command script_check_id `psigma.fst
+run_command script_check_id `psigma.snd
+run_command script_check_id `simp
+run_command script_check_id `singleton
+run_command script_check_id `sizeof
+run_command script_check_id `smt.array
+run_command script_check_id `smt.select
+run_command script_check_id `smt.store
+run_command script_check_id `smt.prove
+run_command script_check_id `string
+run_command script_check_id `string.empty
+run_command script_check_id `string.str
+run_command script_check_id `string.empty_ne_str
+run_command script_check_id `string.str_ne_empty
+run_command script_check_id `string.str_ne_str_left
+run_command script_check_id `string.str_ne_str_right
+run_command script_check_id `sub
+run_command script_check_id `subsingleton
+run_command script_check_id `subsingleton.elim
+run_command script_check_id `subsingleton.helim
+run_command script_check_id `subtype
+run_command script_check_id `subtype.tag
+run_command script_check_id `subtype.elt_of
+run_command script_check_id `subtype.rec
+run_command script_check_id `sum
+run_command script_check_id `sum.cases_on
+run_command script_check_id `sum.inl
+run_command script_check_id `sum.inr
+run_command script_check_id `psum
+run_command script_check_id `psum.cases_on
+run_command script_check_id `psum.inl
+run_command script_check_id `psum.inr
+run_command script_check_id `smt_state.mk
+run_command script_check_id `smt_tactic.execute
+run_command script_check_id `smt_tactic.execute_with
+run_command script_check_id `tactic
+run_command script_check_id `tactic.eval_expr
+run_command script_check_id `tactic.constructor
+run_command script_check_id `tactic.step
+run_command script_check_id `tactic.to_expr
+run_command script_check_id `tactic.skip
+run_command script_check_id `tactic.try
+run_command script_check_id `tactic.triv
+run_command script_check_id `tactic.interactive
+run_command script_check_id `tactic.interactive.exact
+run_command script_check_id `trivial
+run_command script_check_id `thunk
+run_command script_check_id `to_fmt
+run_command script_check_id `to_string
+run_command script_check_id `trans_rel_left
+run_command script_check_id `trans_rel_right
+run_command script_check_id `true
+run_command script_check_id `true.intro
+run_command script_check_id `unification_hint
+run_command script_check_id `unification_hint.mk
+run_command script_check_id `unification_constraint
+run_command script_check_id `unification_constraint.mk
+run_command script_check_id `unit
+run_command script_check_id `unit.cases_on
+run_command script_check_id `unit.star
+run_command script_check_id `user_attribute
+run_command script_check_id `vm_monitor
+run_command script_check_id `weak_order
+run_command script_check_id `well_founded
+run_command script_check_id `xor
+run_command script_check_id `zero
+run_command script_check_id `zero_le_one
+run_command script_check_id `zero_lt_one
+run_command script_check_id `zero_mul