diff --git a/src/library/util.cpp b/src/library/util.cpp
index 2ad2410a69..ce9ebb3d2b 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -106,6 +106,18 @@ bool is_inductive_predicate(environment const & env, name const & n) {
     return is_zero(get_datatype_level(env.get(n).get_type()));
 }
 
+void get_intro_rule_names(environment const & env, name const & n, buffer<name> & result) {
+    if (auto decls = inductive::is_inductive_decl(env, n)) {
+        for (inductive::inductive_decl const & decl : std::get<2>(*decls)) {
+            if (inductive::inductive_decl_name(decl) == n) {
+                for (inductive::intro_rule const & ir : inductive::inductive_decl_intros(decl))
+                    result.push_back(inductive::intro_rule_name(ir));
+                return;
+            }
+        }
+    }
+}
+
 expr instantiate_univ_param (expr const & e, name const & p, level const & l) {
     return instantiate_univ_params(e, to_list(p), to_list(l));
 }
diff --git a/src/library/util.h b/src/library/util.h
index b8637b9d7b..daf50a8466 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -39,6 +39,11 @@ bool is_reflexive_datatype(type_checker & tc, name const & n);
 */
 bool is_inductive_predicate(environment const & env, name const & n);
 
+/** \brief Store in \c result the introduction rules of the given inductive datatype.
+    \remark this procedure does nothing if \c n is not an inductive datatype.
+*/
+void get_intro_rule_names(environment const & env, name const & n, buffer<name> & result);
+
 /** \brief "Consume" Pi-type \c type. This procedure creates local constants based on the domain of \c type
     and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
     binder_info, otherwise the procedure uses the one attached in the domain.