diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 6071f1d97..3c3a6120b 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -278,6 +278,18 @@ theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false
 := boolext (λ H, absurd (and_eliml H) (and_elimr H))
            (λ H, false_elim (a ∧ ¬ a) H)
 
+theorem imp_truer (a : Bool) : (a → true) == true
+:= case (λ x, (x → true) == true) trivial trivial a
+
+theorem imp_truel (a : Bool) : (true → a) == a
+:= case (λ x, (true → x) == x) trivial trivial a
+
+theorem imp_falser (a : Bool) : (a → false) == ¬ a
+:= refl _
+
+theorem imp_falsel (a : Bool) : (false → a) == true
+:= case (λ x, (false → x) == true) trivial trivial a
+
 theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
 := case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b))
         (case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y))   trivial trivial b)
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 072916dc7..f6bc2514c 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index 74ad1fb02..f4101dfb0 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -79,6 +79,10 @@ MK_CONSTANT(and_truel_fn, name("and_truel"));
 MK_CONSTANT(and_falsel_fn, name("and_falsel"));
 MK_CONSTANT(and_falser_fn, name("and_falser"));
 MK_CONSTANT(and_absurd_fn, name("and_absurd"));
+MK_CONSTANT(imp_truer_fn, name("imp_truer"));
+MK_CONSTANT(imp_truel_fn, name("imp_truel"));
+MK_CONSTANT(imp_falser_fn, name("imp_falser"));
+MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
 MK_CONSTANT(not_and_fn, name("not_and"));
 MK_CONSTANT(not_and_elim_fn, name("not_and_elim"));
 MK_CONSTANT(not_or_fn, name("not_or"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index 25ce05b1d..8e9768323 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -228,6 +228,18 @@ inline expr mk_and_falser_th(expr const & e1) { return mk_app({mk_and_falser_fn(
 expr mk_and_absurd_fn();
 bool is_and_absurd_fn(expr const & e);
 inline expr mk_and_absurd_th(expr const & e1) { return mk_app({mk_and_absurd_fn(), e1}); }
+expr mk_imp_truer_fn();
+bool is_imp_truer_fn(expr const & e);
+inline expr mk_imp_truer_th(expr const & e1) { return mk_app({mk_imp_truer_fn(), e1}); }
+expr mk_imp_truel_fn();
+bool is_imp_truel_fn(expr const & e);
+inline expr mk_imp_truel_th(expr const & e1) { return mk_app({mk_imp_truel_fn(), e1}); }
+expr mk_imp_falser_fn();
+bool is_imp_falser_fn(expr const & e);
+inline expr mk_imp_falser_th(expr const & e1) { return mk_app({mk_imp_falser_fn(), e1}); }
+expr mk_imp_falsel_fn();
+bool is_imp_falsel_fn(expr const & e);
+inline expr mk_imp_falsel_th(expr const & e1) { return mk_app({mk_imp_falsel_fn(), e1}); }
 expr mk_not_and_fn();
 bool is_not_and_fn(expr const & e);
 inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); }