diff --git a/src/library/eqn_lemmas.cpp b/src/library/eqn_lemmas.cpp
index c7e30f3a24..543aba7aa7 100644
--- a/src/library/eqn_lemmas.cpp
+++ b/src/library/eqn_lemmas.cpp
@@ -63,7 +63,7 @@ environment add_eqn_lemma_core(environment const & env, name const & eqn_lemma)
 
 environment add_eqn_lemma(environment const & env, name const & eqn_lemma) {
     environment new_env = add_eqn_lemma_core(env, eqn_lemma);
-    return module::add(env, *g_eqn_lemmas_key, [=](environment const &, serializer & s) { s << eqn_lemma; });
+    return module::add(new_env, *g_eqn_lemmas_key, [=](environment const &, serializer & s) { s << eqn_lemma; });
 }
 
 void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_only, buffer<simp_lemma> & result) {
@@ -76,6 +76,11 @@ void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_o
     }
 }
 
+bool has_eqn_lemmas(environment const & env, name const & cname) {
+    eqn_lemmas_ext const & ext = get_extension(env);
+    return ext.m_lemmas.contains(cname);
+}
+
 static void eqn_lemmas_reader(deserializer & d, shared_environment & senv,
                               std::function<void(asynch_update_fn const &)> &,
                               std::function<void(delayed_update_fn const &)> &) {
diff --git a/src/library/eqn_lemmas.h b/src/library/eqn_lemmas.h
index 9b80d306a6..138e2f02fc 100644
--- a/src/library/eqn_lemmas.h
+++ b/src/library/eqn_lemmas.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 environment add_eqn_lemma(environment const & env, name const & eqn_lemma);
+bool has_eqn_lemmas(environment const & env, name const & cname);
 void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_only, buffer<simp_lemma> & result);
 void initialize_eqn_lemmas();
 void finalize_eqn_lemmas();