diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
index 7b918ae74..c85d1695f 100644
--- a/src/builtin/CMakeLists.txt
+++ b/src/builtin/CMakeLists.txt
@@ -100,4 +100,5 @@ update_interface("kernel.olean"       "kernel" "-n")
 update_interface("Nat.olean"          "library/arith" "-n")
 update_interface("Int.olean"          "library/arith" "")
 update_interface("Real.olean"         "library/arith" "")
-update_interface("if_then_else.olean" "library" "")
\ No newline at end of file
+update_interface("if_then_else.olean" "library" "")
+update_interface("heq.olean"          "library" "")
\ No newline at end of file
diff --git a/src/library/heq_decls.cpp b/src/library/heq_decls.cpp
new file mode 100644
index 000000000..844422c2b
--- /dev/null
+++ b/src/library/heq_decls.cpp
@@ -0,0 +1,21 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+*/
+// Automatically generated file, DO NOT EDIT
+#include "kernel/environment.h"
+#include "kernel/decl_macros.h"
+namespace lean {
+MK_CONSTANT(heq_fn, name("heq"));
+MK_CONSTANT(heq_eq_fn, name("heq_eq"));
+MK_CONSTANT(to_eq_fn, name("to_eq"));
+MK_CONSTANT(to_heq_fn, name("to_heq"));
+MK_CONSTANT(hrefl_fn, name("hrefl"));
+MK_CONSTANT(hsymm_fn, name("hsymm"));
+MK_CONSTANT(htrans_fn, name("htrans"));
+MK_CONSTANT(hcongr_fn, name("hcongr"));
+MK_CONSTANT(TypeM, name("TypeM"));
+MK_CONSTANT(hfunext_fn, name("hfunext"));
+MK_CONSTANT(hpiext_fn, name("hpiext"));
+MK_CONSTANT(hallext_fn, name("hallext"));
+}
diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h
new file mode 100644
index 000000000..83533e845
--- /dev/null
+++ b/src/library/heq_decls.h
@@ -0,0 +1,46 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+*/
+// Automatically generated file, DO NOT EDIT
+#include "kernel/expr.h"
+namespace lean {
+expr mk_heq_fn();
+bool is_heq_fn(expr const & e);
+inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)); }
+inline expr mk_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq_fn(), e1, e2, e3, e4}); }
+expr mk_heq_eq_fn();
+bool is_heq_eq_fn(expr const & e);
+inline expr mk_heq_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_heq_eq_fn(), e1, e2, e3}); }
+expr mk_to_eq_fn();
+bool is_to_eq_fn(expr const & e);
+inline bool is_to_eq(expr const & e) { return is_app(e) && is_to_eq_fn(arg(e, 0)); }
+inline expr mk_to_eq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_eq_fn(), e1, e2, e3, e4}); }
+expr mk_to_heq_fn();
+bool is_to_heq_fn(expr const & e);
+inline bool is_to_heq(expr const & e) { return is_app(e) && is_to_heq_fn(arg(e, 0)); }
+inline expr mk_to_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_heq_fn(), e1, e2, e3, e4}); }
+expr mk_hrefl_fn();
+bool is_hrefl_fn(expr const & e);
+inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); }
+expr mk_hsymm_fn();
+bool is_hsymm_fn(expr const & e);
+inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); }
+expr mk_htrans_fn();
+bool is_htrans_fn(expr const & e);
+inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_htrans_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
+expr mk_hcongr_fn();
+bool is_hcongr_fn(expr const & e);
+inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); }
+expr mk_TypeM();
+bool is_TypeM(expr const & e);
+expr mk_hfunext_fn();
+bool is_hfunext_fn(expr const & e);
+inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
+expr mk_hpiext_fn();
+bool is_hpiext_fn(expr const & e);
+inline expr mk_hpiext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hpiext_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_hallext_fn();
+bool is_hallext_fn(expr const & e);
+inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); }
+}