diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index ceb83d1f0..8ba1d3b78 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -246,7 +246,8 @@ static int expr_tostring(lua_State * L) {
     return push_string(L, out.str().c_str());
 }
 
-static int expr_eq(lua_State * L) { return push_boolean(L, to_expr(L, 1) == to_expr(L, 2)); }
+static int expr_is_equal(lua_State * L) { return push_boolean(L, to_expr(L, 1) == to_expr(L, 2)); }
+static int expr_is_bi_equal(lua_State * L) { return push_boolean(L, is_bi_equal(to_expr(L, 1), to_expr(L, 2))); }
 static int expr_lt(lua_State * L) { return push_boolean(L, to_expr(L, 1) < to_expr(L, 2)); }
 static int expr_mk_constant(lua_State * L) {
     int nargs = lua_gettop(L);
@@ -551,7 +552,7 @@ static int expr_tag(lua_State * L) {
 static const struct luaL_Reg expr_m[] = {
     {"__gc",             expr_gc}, // never throws
     {"__tostring",       safe_function<expr_tostring>},
-    {"__eq",             safe_function<expr_eq>},
+    {"__eq",             safe_function<expr_is_equal>},
     {"__lt",             safe_function<expr_lt>},
     {"__call",           safe_function<expr_mk_app>},
     {"kind",             safe_function<expr_get_kind>},
@@ -597,6 +598,8 @@ static const struct luaL_Reg expr_m[] = {
     {"occurs",           safe_function<expr_occurs>},
     {"is_eqp",           safe_function<expr_is_eqp>},
     {"is_lt",            safe_function<expr_is_lt>},
+    {"is_equal",         safe_function<expr_is_equal>},
+    {"is_bi_equal",      safe_function<expr_is_bi_equal>},
     {"hash",             safe_function<expr_hash>},
     {"tag",              safe_function<expr_tag>},
     {"set_tag",          safe_function<expr_set_tag>},
diff --git a/tests/lua/tc3.lua b/tests/lua/tc3.lua
index d9c8ba8c2..6f487f45e 100644
--- a/tests/lua/tc3.lua
+++ b/tests/lua/tc3.lua
@@ -8,7 +8,11 @@ local T1  = mk_pi("A", Type, mk_arrow(Var(0), Var(1)), binder_info(true))
 local T2  = mk_pi("A", Type, mk_arrow(Var(0), Var(1)))
 print(T1)
 print(T2)
+assert(T1 == T2) -- The default equality ignores binder information
+assert(not (T1:is_bi_equal(T2)))
 print(tc:check(t1))
 print(tc:check(t2))
 assert(tc:check(t1):binder_info():is_implicit())
 assert(not tc:check(t2):binder_info():is_implicit())
+assert(tc:check(t1):is_bi_equal(T1))
+assert(tc:check(t2):is_bi_equal(T2))