diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index ea3952b10..ab7ead794 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <vector>
 #include <limits>
+#include "util/thread.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
 
@@ -28,18 +29,53 @@ environment_header::environment_header(unsigned trust_lvl, bool prop_proof_irrel
 
 environment_extension::~environment_extension() {}
 
-environment_id::environment_id():m_trail(0, list<unsigned>()) {}
+struct environment_id::path {
+    unsigned m_next_depth;
+    unsigned m_start_depth;
+    mutex    m_mutex;
+    path *   m_prev;
+    MK_LEAN_RC(); // Declare m_rc counter
+    void dealloc() { delete this; }
 
-environment_id::environment_id(environment_id const & ancestor, bool):m_trail(car(ancestor.m_trail) + 1, ancestor.m_trail) {}
+    path():m_next_depth(1), m_start_depth(0), m_prev(nullptr), m_rc(1) {}
+    path(unsigned start_depth, path * prev):m_next_depth(start_depth + 1), m_start_depth(start_depth), m_prev(prev), m_rc(1) {
+        if (prev) prev->inc_ref();
+    }
+    ~path() { if (m_prev) m_prev->dec_ref(); }
+};
 
+environment_id::environment_id():m_ptr(new path()), m_depth(0) {}
+environment_id::environment_id(environment_id const & ancestor, bool) {
+    if (ancestor.m_depth == std::numeric_limits<unsigned>::max())
+        throw exception("maximal depth in is_descendant tree has been reached, use 'forget' method to workaround this limitation");
+    unique_lock<mutex> lock(ancestor.m_ptr->m_mutex);
+    if (ancestor.m_ptr->m_next_depth == ancestor.m_depth + 1) {
+        m_ptr   = ancestor.m_ptr;
+        m_depth = ancestor.m_depth + 1;
+        m_ptr->m_next_depth++;
+        m_ptr->inc_ref();
+    } else {
+        m_ptr   = new path(ancestor.m_depth+1, ancestor.m_ptr);
+        m_depth = ancestor.m_depth + 1;
+    }
+    lean_assert(m_depth == ancestor.m_depth+1);
+    lean_assert(m_ptr->m_next_depth == m_depth+1);
+}
+environment_id::environment_id(environment_id const & id):m_ptr(id.m_ptr), m_depth(id.m_depth) { if (m_ptr) m_ptr->inc_ref(); }
+environment_id::environment_id(environment_id && id):m_ptr(id.m_ptr), m_depth(id.m_depth) { id.m_ptr = nullptr; }
+environment_id::~environment_id() { if (m_ptr) m_ptr->dec_ref(); }
+environment_id & environment_id::operator=(environment_id const & s) { m_depth = s.m_depth; LEAN_COPY_REF(s); }
+environment_id & environment_id::operator=(environment_id && s) { m_depth = s.m_depth; LEAN_MOVE_REF(s); }
 bool environment_id::is_descendant(environment_id const & id) const {
-    list<unsigned> const * it = &m_trail;
-    while (!is_nil(*it)) {
-        if (is_eqp(*it, id.m_trail))
+    if (m_depth < id.m_depth)
+        return false;
+    path * p = m_ptr;
+    while (p != nullptr) {
+        if (p == id.m_ptr)
             return true;
-        if (car(*it) < car(id.m_trail))
+        if (p->m_start_depth <= id.m_depth)
             return false;
-        it = &cdr(*it);
+        p = p->m_prev;
     }
     return false;
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index c41e4ae9c..260448532 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -74,12 +74,13 @@ public:
 
 typedef std::vector<std::shared_ptr<environment_extension const>> environment_extensions;
 
-/**
-   \brief environment identifier that allows us to track descendants of a given environment.
-*/
+/** \brief environment identifier for tracking descendants of a given environment. */
 class environment_id {
+    friend class environment_id_tester;
     friend class environment; // Only the environment class can create object of this type.
-    list<unsigned> m_trail; //!< trail of ancestors. The unsigned value is redundant, it store the depth of the trail.
+    struct path;
+    path *   m_ptr;
+    unsigned m_depth;
     /**
         \brief Create an identifier for an environment that is a direct descendant of the given one.
         The bool field is just to make sure this constructor is not confused with a copy constructor
@@ -90,6 +91,12 @@ class environment_id {
     /** Create an identifier for an environment that is a direct descendant of the given one. */
     static environment_id mk_descendant(environment_id const & ancestor) { return environment_id(ancestor, true); }
 public:
+    environment_id(environment_id const & id);
+    environment_id(environment_id && id);
+    ~environment_id();
+    environment_id & operator=(environment_id const & s);
+    environment_id & operator=(environment_id && s);
+
     /** \brief Return true iff this object is a descendant of the given one. */
     bool is_descendant(environment_id const & id) const;
 };
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index db86c428a..d95f252b9 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <vector>
 #include "util/test.h"
 #include "util/exception.h"
 #include "util/trace.h"
@@ -158,11 +159,88 @@ static void tst4() {
     }
 }
 
+namespace lean {
+class environment_id_tester {
+public:
+    static void tst1() {
+        environment_id id1;
+        environment_id id2 = environment_id::mk_descendant(id1);
+        environment_id id3 = environment_id::mk_descendant(id2);
+        environment_id id4 = environment_id::mk_descendant(id1);
+        environment_id id5 = environment_id::mk_descendant(id3);
+        environment_id id6 = environment_id::mk_descendant(id4);
+        environment_id id7 = environment_id::mk_descendant(id3);
+        environment_id id8 = environment_id::mk_descendant(id7);
+        lean_assert(id1.is_descendant(id1));
+        lean_assert(id2.is_descendant(id1));
+        lean_assert(!id1.is_descendant(id2));
+        lean_assert(id3.is_descendant(id1));
+        lean_assert(id3.is_descendant(id2));
+        lean_assert(id4.is_descendant(id1));
+        lean_assert(!id4.is_descendant(id2));
+        lean_assert(!id4.is_descendant(id3));
+        lean_assert(id5.is_descendant(id3));
+        lean_assert(!id5.is_descendant(id4));
+        lean_assert(id6.is_descendant(id4));
+        lean_assert(!id6.is_descendant(id5));
+        lean_assert(id5.is_descendant(id1));
+        lean_assert(id6.is_descendant(id1));
+        lean_assert(id7.is_descendant(id3));
+        lean_assert(id7.is_descendant(id2));
+        lean_assert(id7.is_descendant(id1));
+        lean_assert(!id7.is_descendant(id4));
+        lean_assert(!id7.is_descendant(id5));
+        lean_assert(!id7.is_descendant(id6));
+        lean_assert(id8.is_descendant(id7));
+        lean_assert(id8.is_descendant(id3));
+        lean_assert(id8.is_descendant(id2));
+        lean_assert(id8.is_descendant(id1));
+        lean_assert(!id8.is_descendant(id4));
+        lean_assert(!id8.is_descendant(id5));
+        lean_assert(!id8.is_descendant(id6));
+    }
+
+    static void tst2() {
+        constexpr unsigned num_paths = 50;
+        constexpr unsigned path_len  = 100;
+        std::vector<environment_id> ids[num_paths];
+        for (unsigned i = 0; i < num_paths; i++) {
+            if (i == 0)
+                ids[i].push_back(environment_id());
+            else
+                ids[i].push_back(environment_id::mk_descendant(ids[i-1][1]));
+            for (unsigned j = 0; j < path_len; j++) {
+                ids[i].push_back(environment_id::mk_descendant(ids[i].back()));
+            }
+        }
+        for (unsigned i = 0; i < num_paths; i++) {
+            for (unsigned j = 0; j < path_len; j++) {
+                for (unsigned k = 0; k < i; k++) {
+                    lean_assert(ids[i][j].is_descendant(ids[k][1]));
+                    lean_assert(ids[i][j].is_descendant(ids[k][0]));
+                    lean_assert(!ids[k][1].is_descendant(ids[i][j]));
+                    lean_assert(!ids[k][0].is_descendant(ids[i][j]));
+                    for (unsigned s = 2; s < path_len; s++) {
+                        lean_assert(!ids[i][j].is_descendant(ids[k][s]));
+                    }
+                }
+                for (unsigned k = 0; k < j; k++) {
+                    lean_assert(ids[i][j].is_descendant(ids[i][k]));
+                    lean_assert(!ids[i][k].is_descendant(ids[i][j]));
+                }
+            }
+        }
+    }
+};
+}
+
 int main() {
     save_stack_info();
     tst1();
     tst2();
     tst3();
     tst4();
+    environment_id_tester::tst1();
+    environment_id_tester::tst2();
     return has_violations() ? 1 : 0;
 }