diff --git a/src/library/util.cpp b/src/library/util.cpp
index 4424e7607..d7c72dc06 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -21,6 +21,16 @@ Author: Leonardo de Moura
 #include "library/projection.h"
 
 namespace lean {
+bool is_app_of(expr const & t, name const & f_name) {
+    expr const & fn = get_app_fn(t);
+    return is_constant(fn) && const_name(fn) == f_name;
+}
+
+bool is_app_of(expr const & t, name const & f_name, unsigned nargs) {
+    expr const & fn = get_app_fn(t);
+    return is_constant(fn) && const_name(fn) == f_name && get_app_num_args(t) == nargs;
+}
+
 bool is_standard(environment const & env) {
     return env.prop_proof_irrel() && env.impredicative();
 }
diff --git a/src/library/util.h b/src/library/util.h
index 8bd094476..3bc0d4c5e 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -9,6 +9,11 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 
 namespace lean {
+/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
+bool is_app_of(expr const & t, name const & f_name);
+/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_nargs) */
+bool is_app_of(expr const & t, name const & f_name, unsigned nargs);
+
 typedef std::unique_ptr<type_checker> type_checker_ptr;
 /** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....),
     where \c f is a constant */