diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 381e63018..b9eb8dadd 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -56,4 +56,14 @@ expr FName(std::initializer_list<std::pair<expr const &, expr const &>> const &
 
 MkBinder(Fun);
 MkBinder(Pi);
+
+expr Pi(unsigned num, expr const * locals, expr const & b) {
+    expr r = b;
+    unsigned i = num;
+    while (i > 0) {
+        --i;
+        r = mk_pi(local_pp_name(locals[i]), mlocal_type(locals[i]), abstract(r, locals[i]));
+    }
+    return r;
+}
 }
diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h
index 0045f1fcc..a71594eb7 100644
--- a/src/kernel/abstract.h
+++ b/src/kernel/abstract.h
@@ -55,7 +55,10 @@ inline expr Pi(expr const & n, expr const & t, expr const & b, binder_info const
 }
 inline expr Pi(std::pair<expr const &, expr const &> const & p, expr const & b) { return Pi(p.first, p.second, b); }
 expr Pi(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
-
+/** \brief Create a Pi-expression by abstracting the given local constants over b */
+expr Pi(unsigned num, expr const * locals, expr const & b);
+template<typename T> expr Pi(T const & locals, expr const & b) { return Pi(locals.size(), locals.data(), b); }
+inline expr Pi(expr const & local, expr const & b) { return Pi(1, &local, b); }
 /**
 -   \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x).
 -*/