diff --git a/src/builtin/obj/if_then_else.olean b/src/builtin/obj/if_then_else.olean
index c085ab55a..202e92997 100644
Binary files a/src/builtin/obj/if_then_else.olean and b/src/builtin/obj/if_then_else.olean differ
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 2b7047eca..cf1b7486a 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(library kernel_bindings.cpp deep_copy.cpp
   context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
   fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp
-  hop_match.cpp ite.cpp)
+  hop_match.cpp ite.cpp heq_decls.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/if_then_else_decls.cpp b/src/library/if_then_else_decls.cpp
index 57c5b08dc..91dfc556a 100644
--- a/src/library/if_then_else_decls.cpp
+++ b/src/library/if_then_else_decls.cpp
@@ -12,4 +12,7 @@ MK_CONSTANT(if_a_a_fn, name("if_a_a"));
 MK_CONSTANT(if_congr_fn, name("if_congr"));
 MK_CONSTANT(if_imp_then_fn, name("if_imp_then"));
 MK_CONSTANT(if_imp_else_fn, name("if_imp_else"));
+MK_CONSTANT(app_if_distribute_fn, name("app_if_distribute"));
+MK_CONSTANT(eq_if_distributer_fn, name("eq_if_distributer"));
+MK_CONSTANT(eq_if_distributel_fn, name("eq_if_distributel"));
 }
diff --git a/src/library/if_then_else_decls.h b/src/library/if_then_else_decls.h
index cc511ccca..af787b429 100644
--- a/src/library/if_then_else_decls.h
+++ b/src/library/if_then_else_decls.h
@@ -23,4 +23,13 @@ inline expr mk_if_imp_then_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_if_imp_else_fn();
 bool is_if_imp_else_fn(expr const & e);
 inline expr mk_if_imp_else_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_else_fn(), e1, e2, e3, e4, e5}); }
+expr mk_app_if_distribute_fn();
+bool is_app_if_distribute_fn(expr const & e);
+inline expr mk_app_if_distribute_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_app_if_distribute_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_eq_if_distributer_fn();
+bool is_eq_if_distributer_fn(expr const & e);
+inline expr mk_eq_if_distributer_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributer_fn(), e1, e2, e3, e4, e5}); }
+expr mk_eq_if_distributel_fn();
+bool is_eq_if_distributel_fn(expr const & e);
+inline expr mk_eq_if_distributel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributel_fn(), e1, e2, e3, e4, e5}); }
 }