diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp
index 668c0376d5..1d5adc3038 100644
--- a/src/library/local_context.cpp
+++ b/src/library/local_context.cpp
@@ -136,6 +136,11 @@ optional<local_decl> local_context::get_local_decl_from_user_name(name const & n
     return back_find_if([&](local_decl const & d) { return d.get_pp_name() == n; });
 }
 
+optional<local_decl> local_context::get_last_local_decl() const {
+    if (m_idx2local_decl.empty()) return optional<local_decl>();
+    return optional<local_decl>(m_idx2local_decl.max());
+}
+
 void local_context::for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const {
     m_idx2local_decl.for_each_greater(d.get_idx(), [&](unsigned, local_decl const & d) { return fn(d); });
 }
@@ -307,6 +312,26 @@ format local_context::pp(formatter const & fmt) const {
     return r;
 }
 
+bool local_context::uses_user_name(name const & n) {
+    return static_cast<bool>(m_idx2local_decl.find_if([&](unsigned, local_decl const & d) { return d.get_pp_name() == n; }));
+}
+
+name local_context::get_unused_name(name const & prefix, unsigned & idx) {
+    while (true) {
+        name curr = prefix.append_after(idx);
+        idx++;
+        if (!uses_user_name(curr))
+            return curr;
+    }
+}
+
+name local_context::get_unused_name(name const & suggestion) {
+    if (!uses_user_name(suggestion))
+        return suggestion;
+    unsigned idx = 1;
+    return get_unused_name(suggestion, idx);
+}
+
 void initialize_local_context() {
     g_local_prefix = new name(name::mk_internal_unique_name());
     g_dummy_type   = new expr(mk_constant(name::mk_internal_unique_name()));
diff --git a/src/library/local_context.h b/src/library/local_context.h
index a85461030d..386e014a35 100644
--- a/src/library/local_context.h
+++ b/src/library/local_context.h
@@ -100,6 +100,8 @@ public:
         \remark This method is used to implement tactics such as 'revert'. */
     optional<local_decl> get_local_decl_from_user_name(name const & n) const;
 
+    optional<local_decl> get_last_local_decl() const;
+
     bool rename_user_name(name const & from, name const & to);
 
     /** \brief Execute fn for each local declaration created after \c d. */
@@ -110,6 +112,13 @@ public:
         \pre \c d is in this local context. */
     optional<local_decl> has_dependencies(local_decl const & d) const;
 
+    /** \brief Return an unused hypothesis "user name" with the given prefix, the suffix is an
+        unsigned >= idx. */
+    name get_unused_name(name const & prefix, unsigned & idx);
+    name get_unused_name(name const & suggestion);
+    /** \brief Return true iff the given name is a hypothesis "user name". */
+    bool uses_user_name(name const & n);
+
     /** \brief Remove the given local decl.
         \pre \c d is in this local context, is not frozen, and no other local decl depends on it. */
     void clear(local_decl const & d);