diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 0a23c4ad3b..4661d1bfb6 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -447,6 +447,21 @@ expr const & get_app_args(expr const & e, buffer<expr> & args) {
     return *it;
 }
 
+expr const & get_app_args_at_most(expr const & e, unsigned num, buffer<expr> & args) {
+    unsigned sz = args.size();
+    expr const * it = &e;
+    unsigned i = 0;
+    while (is_app(*it)) {
+        if (i == num)
+            break;
+        args.push_back(app_arg(*it));
+        it = &(app_fn(*it));
+        i++;
+    }
+    std::reverse(args.begin() + sz, args.end());
+    return *it;
+}
+
 expr const & get_app_rev_args(expr const & e, buffer<expr> & args) {
     expr const * it = &e;
     while (is_app(*it)) {
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 87a652058c..df13ae595b 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -567,6 +567,16 @@ inline bool closed(expr const & e) { return !has_free_vars(e); }
     It returns the f.
 */
 expr const & get_app_args(expr const & e, buffer<expr> & args);
+/** \brief Similar to \c get_app_args, but stores at most num args.
+    Examples:
+    1) get_app_args_at_most(f a b c, 2, args);
+    stores {b, c} in args and returns (f a)
+
+    2) get_app_args_at_most(f a b c, 4, args);
+    stores {a, b, c} in args and returns f
+*/
+expr const & get_app_args_at_most(expr const & e, unsigned num, buffer<expr> & args);
+
 /**
    \brief Similar to \c get_app_args, but arguments are stored in reverse order in \c args.
    If e is of the form <tt>(...(f a1) ... an)</tt>, then the procedure stores [an, ..., a1] in \c args.