diff --git a/src/builtin/basic.lean b/src/builtin/basic.lean
index 78eb30943f..d21bff7d3a 100644
--- a/src/builtin/basic.lean
+++ b/src/builtin/basic.lean
@@ -3,9 +3,77 @@ Import macros
 Definition TypeU := (Type U)
 Definition TypeM := (Type M)
 
+Definition implies (a b : Bool) : Bool
+:= if a b true.
+
+Infixr 25 => : implies.
+Infixr 25 ⇒ : implies.
+
+Definition iff (a b : Bool) : Bool
+:= a == b.
+
+Infixr 25 <=> : iff.
+Infixr 25 ⇔ : iff.
+
+Definition not (a : Bool) : Bool
+:= if a false true.
+
+Notation 40 ¬ _ : not.
+
+Definition or (a b : Bool) : Bool
+:= ¬ a ⇒ b.
+
+Infixr 30 || : or.
+Infixr 30 \/ : or.
+Infixr 30 ∨  : or.
+
+Definition and (a b : Bool) : Bool
+:= ¬ (a ⇒ ¬ b).
+
+Infixr 35 && : and.
+Infixr 35 /\ : and.
+Infixr 35 ∧  : and.
+
+(* Forall is a macro for the identifier forall, we use that
+   because the Lean parser has the builtin syntax sugar:
+      forall x : T, P x
+   for
+      (forall T (fun x : T, P x))
+*)
+Definition Forall (A : TypeU) (P : A → Bool) : Bool
+:= P == (λ x : A, true).
+
+Definition Exists (A : TypeU) (P : A → Bool) : Bool
+:= ¬ (Forall A (λ x : A, ¬ (P x))).
+
+Definition eq {A : TypeU} (a b : A) : Bool
+:= a == b.
+
+Infix 50 = : eq.
+
+Axiom MP {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b.
+
+Axiom Discharge {a b : Bool} (H : a → b) : a ⇒ b.
+
+Axiom Case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a.
+
+Axiom Refl {A : TypeU} (a : A) : a == a.
+
+Axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b.
+
 Definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
 := Subst H1 H2.
 
+Axiom Eta {A : TypeU} {B : A → TypeU} (f : Π x : A, B x) : (λ x : A, f x) == f.
+
+Axiom ImpAntisym {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : a == b.
+
+Axiom Abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g.
+
+Axiom HSymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a.
+
+Axiom HTrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c.
+
 Theorem Trivial : true
 := Refl true.
 
diff --git a/src/builtin/basic.olean b/src/builtin/basic.olean
index dde6574e90..c8313c601c 100644
Binary files a/src/builtin/basic.olean and b/src/builtin/basic.olean differ
diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index 5739866b8f..1615e5e67d 100644
--- a/src/frontends/lean/notation.cpp
+++ b/src/frontends/lean/notation.cpp
@@ -22,32 +22,8 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
     env->import_builtin(
         "lean_notation",
         [&]() {
-            add_infix(env, ios, "=",  50, mk_homo_eq_fn());
-            mark_implicit_arguments(env, mk_homo_eq_fn(), 1);
             mark_implicit_arguments(env, mk_if_fn(), 1);
 
-            add_prefix(env, ios, "\u00ac", 40, mk_not_fn());     // "¬"
-            add_infixr(env, ios, "&&", 35, mk_and_fn());         // "&&"
-            add_infixr(env, ios, "/\\", 35, mk_and_fn());        // "/\"
-            add_infixr(env, ios, "\u2227", 35, mk_and_fn());     // "∧"
-            add_infixr(env, ios, "||", 30, mk_or_fn());          // "||"
-            add_infixr(env, ios, "\\/", 30, mk_or_fn());         // "\/"
-            add_infixr(env, ios, "\u2228", 30, mk_or_fn());      // "∨"
-            add_infixr(env, ios, "=>", 25, mk_implies_fn());     // "=>"
-            add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒"
-            add_infixr(env, ios, "<=>", 25, mk_iff_fn());        // "<=>"
-            add_infixr(env, ios, "\u21D4", 25, mk_iff_fn());     // "⇔"
-
-            // implicit arguments for builtin axioms
-            mark_implicit_arguments(env, mk_mp_fn(), 2);
-            mark_implicit_arguments(env, mk_discharge_fn(), 2);
-            mark_implicit_arguments(env, mk_refl_fn(), 1);
-            mark_implicit_arguments(env, mk_subst_fn(), 4);
-            mark_implicit_arguments(env, mk_eta_fn(), 2);
-            mark_implicit_arguments(env, mk_abst_fn(), 4);
-            mark_implicit_arguments(env, mk_imp_antisym_fn(), 2);
-            mark_implicit_arguments(env, mk_hsymm_fn(), 4);
-            mark_implicit_arguments(env, mk_htrans_fn(), 6);
 
             if (kernel_only)
                 return;
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 95a6868e9a..62b6f4412c 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -190,85 +190,10 @@ void import_kernel(environment const & env) {
          [&]() {
             env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
             env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
-
-            expr p1        = Bool >> Bool;
-            expr p2        = Bool >> p1;
-            expr f         = Const("f");
-            expr g         = Const("g");
-            expr a         = Const("a");
-            expr b         = Const("b");
-            expr c         = Const("c");
-            expr x         = Const("x");
-            expr y         = Const("y");
-            expr A         = Const("A");
-            expr A_pred    = A >> Bool;
-            expr B         = Const("B");
-            expr C         = Const("C");
-            expr q_type    = Pi({A, TypeU}, A_pred >> Bool);
-            expr piABx     = Pi({x, A}, B(x));
-            expr A_arrow_u = A >> TypeU;
-            expr P         = Const("P");
-            expr H         = Const("H");
-            expr H1        = Const("H1");
-            expr H2        = Const("H2");
-
             env->add_builtin(mk_bool_type());
             env->add_builtin(mk_bool_value(true));
             env->add_builtin(mk_bool_value(false));
             env->add_builtin(mk_if_fn());
-
-            // implies(x, y) := if x y True
-            env->add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
-
-            // iff(x, y) := x = y
-            env->add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
-
-            // not(x) := if x False True
-            env->add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
-
-            // or(x, y) := Not(x) => y
-            env->add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y)));
-
-            // and(x, y) := Not(x => Not(y))
-            env->add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y)))));
-
-            // forall : Pi (A : Type u), (A -> Bool) -> Bool
-            env->add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
-            // TODO(Leo): introduce epsilon
-            env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
-
-            // homogeneous equality
-            env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y)));
-
-            // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
-            env->add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
-
-            // Discharge : Pi (a b : Bool) (H : a -> b), a => b
-            env->add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b)));
-
-            // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a
-            env->add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a)));
-
-            // Refl : Pi (A : Type u) (a : A), a = a
-            env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
-
-            // Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
-            env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b)));
-
-            // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f
-            env->add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f)));
-
-            // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
-            env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
-
-            // Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g
-            env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g)));
-
-            // HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a
-            env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a)));
-
-            // HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
-            env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
         });
 }
 }
diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp
index c85ec2dfd3..5701a4c14c 100644
--- a/src/tests/library/arith.cpp
+++ b/src/tests/library/arith.cpp
@@ -16,9 +16,8 @@ using namespace lean;
 
 static void tst0() {
     environment env;
+    init_frontend(env);
     normalizer  norm(env);
-    import_kernel(env);
-    import_arith(env);
     env->add_var("n", Nat);
     expr n = Const("n");
     lean_assert_eq(mk_nat_type(), Nat);
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 48bf9162c6..175020fcdc 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-@Subst : Π (A : (Type U)) (a b : A) (P : A → Bool), P a → a == b → P b
+@Subst : Π (A : TypeU) (a b : A) (P : A → Bool), P a → a == b → P b
   Proved: EM2
 EM2 : Π a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a