diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
index 7d38c619a..7f2cd0e2a 100644
--- a/src/kernel/arith/arith.cpp
+++ b/src/kernel/arith/arith.cpp
@@ -123,9 +123,9 @@ public:
 };
 MK_BUILTIN(nat_le_fn, nat_le_value);
 
-MK_CONSTANT(nat_ge_fn, name(name("Nat"), "ge"));
-MK_CONSTANT(nat_lt_fn, name(name("Nat"), "lt"));
-MK_CONSTANT(nat_gt_fn, name(name("Nat"), "gt"));
+MK_CONSTANT(nat_ge_fn, name({"Nat", "ge"}));
+MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"}));
+MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"}));
 // =======================================
 
 // =======================================
@@ -198,16 +198,13 @@ struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1
 typedef int_bin_op<int_add_name, int_add_eval> int_add_value;
 MK_BUILTIN(int_add_fn, int_add_value);
 
-constexpr char int_sub_name[] = "sub";
-struct int_sub_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 - v2; }; };
-typedef int_bin_op<int_sub_name, int_sub_eval> int_sub_value;
-MK_BUILTIN(int_sub_fn, int_sub_value);
-
 constexpr char int_mul_name[] = "mul";
 struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
 typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
 MK_BUILTIN(int_mul_fn, int_mul_value);
 
+MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
+
 constexpr char int_div_name[] = "div";
 struct int_div_eval {
     mpz operator()(mpz const & v1, mpz const & v2) {
@@ -244,9 +241,9 @@ public:
     virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(int_le_fn, int_le_value);
-MK_CONSTANT(int_ge_fn, name(name("Int"), "ge"));
-MK_CONSTANT(int_lt_fn, name(name("Int"), "lt"));
-MK_CONSTANT(int_gt_fn, name(name("Int"), "gt"));
+MK_CONSTANT(int_ge_fn, name({"Int", "ge"}));
+MK_CONSTANT(int_lt_fn, name({"Int", "lt"}));
+MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
 // =======================================
 
 // =======================================
@@ -319,16 +316,13 @@ struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v
 typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
 MK_BUILTIN(real_add_fn, real_add_value);
 
-constexpr char real_sub_name[] = "sub";
-struct real_sub_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 - v2; }; };
-typedef real_bin_op<real_sub_name, real_sub_eval> real_sub_value;
-MK_BUILTIN(real_sub_fn, real_sub_value);
-
 constexpr char real_mul_name[] = "mul";
 struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; };
 typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
 MK_BUILTIN(real_mul_fn, real_mul_value);
 
+MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
+
 constexpr char real_div_name[] = "div";
 struct real_div_eval {
     mpq operator()(mpq const & v1, mpq const & v2) {
@@ -365,9 +359,9 @@ public:
     virtual unsigned hash() const { return m_name.hash(); }
 };
 MK_BUILTIN(real_le_fn, real_le_value);
-MK_CONSTANT(real_ge_fn, name(name("Real"), "ge"));
-MK_CONSTANT(real_lt_fn, name(name("Real"), "lt"));
-MK_CONSTANT(real_gt_fn, name(name("Real"), "gt"));
+MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
+MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
+MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
 // =======================================
 
 // =======================================
@@ -425,23 +419,27 @@ MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
 // =======================================
 
 void add_arith_theory(environment & env) {
-    expr p_nn = Nat >> (Nat >> Bool);
-    expr p_ii = Int >> (Int >> Bool);
-    expr p_rr = Real >> (Real >> Bool);
+    expr nn_b = Nat >> (Nat >> Bool);
+    expr ii_b = Int >> (Int >> Bool);
+    expr ii_i = Int >> (Int >> Int);
+    expr rr_b = Real >> (Real >> Bool);
+    expr rr_r = Real >> (Real >> Real);
     expr x    = Const("x");
     expr y    = Const("y");
 
-    env.add_definition(nat_ge_fn_name, p_nn, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
-    env.add_definition(nat_lt_fn_name, p_nn, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
-    env.add_definition(nat_gt_fn_name, p_nn, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
+    env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
+    env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
+    env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
 
-    env.add_definition(int_ge_fn_name, p_ii, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
-    env.add_definition(int_lt_fn_name, p_ii, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
-    env.add_definition(int_gt_fn_name, p_ii, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
+    env.add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(mk_int_value(-1), y))));
+    env.add_definition(int_ge_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, iLe(y, x)));
+    env.add_definition(int_lt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
+    env.add_definition(int_gt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
 
-    env.add_definition(real_ge_fn_name, p_rr, Fun({{x, Real}, {y, Real}}, rLe(y, x)));
-    env.add_definition(real_lt_fn_name, p_rr, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
-    env.add_definition(real_gt_fn_name, p_rr, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
+    env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(mk_real_value(-1), y))));
+    env.add_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));
+    env.add_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
+    env.add_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
 
     env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
 }
diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp
index 744710d87..847af93b1 100644
--- a/src/tests/kernel/arith.cpp
+++ b/src/tests/kernel/arith.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "builtin.h"
 #include "arith.h"
 #include "normalizer.h"
+#include "toplevel.h"
 #include "abstract.h"
 #include "printer.h"
 #include "test.h"
@@ -56,7 +57,7 @@ static void tst3() {
 }
 
 static void tst4() {
-    environment env;
+    environment env = mk_toplevel();
     expr e = iSub(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
@@ -68,7 +69,7 @@ static void tst4() {
     expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30))));
     std::cout << e2 << " --> " << normalize(e2, env) << "\n";
     lean_assert(infer_type(e2, env) == (Int >> Int));
-    lean_assert(normalize(e2, env) == Fun("a", Int, iSub(Const("a"), iVal(-20))));
+    lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(20))));
 }
 
 static void tst5() {
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 863d8c55d..7b4c9f2f0 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -111,7 +111,7 @@ static void tst3() {
 }
 
 static void tst4() {
-    environment env;
+    environment env = mk_toplevel();
     env.add_definition("a", Int, iVal(1), true); // add opaque definition
     expr t = iAdd(Const("a"), iVal(1));
     std::cout << t << " --> " << normalize(t, env) << "\n";
@@ -119,7 +119,7 @@ static void tst4() {
     env.add_definition("b", Int, iAdd(Const("a"), iVal(1)));
     expr t2 = iSub(Const("b"), iVal(9));
     std::cout << t2 << " --> " << normalize(t2, env) << "\n";
-    lean_assert(normalize(t2, env) == iSub(iAdd(Const("a"), iVal(1)), iVal(9)));
+    lean_assert(normalize(t2, env) == iAdd(iAdd(Const("a"), iVal(1)), iVal(-9)));
 }
 
 static void tst5() {