diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 4389df644..467470678 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,7 +1,7 @@
 add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
-  type_checker.cpp builtin.cpp occurs.cpp metavar.cpp trace.cpp
+  type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
   unification_constraint.cpp printer.cpp formatter.cpp
-  kernel_exception.cpp type_checker_trace.cpp pos_info_provider.cpp)
+  kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/trace.cpp b/src/kernel/justification.cpp
similarity index 63%
rename from src/kernel/trace.cpp
rename to src/kernel/justification.cpp
index 37c4d6973..9076ec1ce 100644
--- a/src/kernel/trace.cpp
+++ b/src/kernel/justification.cpp
@@ -6,10 +6,10 @@ Author: Leonardo de Moura
 */
 #include <set>
 #include "util/buffer.h"
-#include "kernel/trace.h"
+#include "kernel/justification.h"
 
 namespace lean {
-void trace_cell::add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
+void justification_cell::add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
     if (!p || !e)
         return;
     format f = p->pp(e);
@@ -19,41 +19,41 @@ void trace_cell::add_pos_info(format & r, expr const & e, pos_info_provider cons
     r += space();
 }
 
-format trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const {
+format justification_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const {
     format r;
     add_pos_info(r, get_main_expr(), p);
     r += pp_header(fmt, opts);
     if (display_children) {
-        buffer<trace_cell *> children;
+        buffer<justification_cell *> children;
         get_children(children);
         unsigned indent = get_pp_indent(opts);
-        for (trace_cell * child : children) {
+        for (justification_cell * child : children) {
             r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children)));
         }
     }
     return r;
 }
 
-bool trace::has_children() const {
-    buffer<trace_cell *> r;
+bool justification::has_children() const {
+    buffer<justification_cell *> r;
     get_children(r);
     return !r.empty();
 }
 
-bool depends_on(trace const & t, trace const & d) {
-    buffer<trace_cell *>   todo;
-    std::set<trace_cell *> visited;
-    buffer<trace_cell *>   children;
+bool depends_on(justification const & t, justification const & d) {
+    buffer<justification_cell *>   todo;
+    std::set<justification_cell *> visited;
+    buffer<justification_cell *>   children;
     todo.push_back(t.raw());
     while (!todo.empty()) {
-        trace_cell * curr = todo.back();
+        justification_cell * curr = todo.back();
         todo.pop_back();
         if (curr == d.raw()) {
             return true;
         } else {
             children.clear();
             curr->get_children(children);
-            for (trace_cell * child : children) {
+            for (justification_cell * child : children) {
                 if (child->is_shared()) {
                     if (visited.find(child) == visited.end()) {
                         visited.insert(child);
diff --git a/src/kernel/trace.h b/src/kernel/justification.h
similarity index 50%
rename from src/kernel/trace.h
rename to src/kernel/justification.h
index f14a627e9..e8388f282 100644
--- a/src/kernel/trace.h
+++ b/src/kernel/justification.h
@@ -15,54 +15,54 @@ Author: Leonardo de Moura
 #include "kernel/pos_info_provider.h"
 
 namespace lean {
-class trace;
+class justification;
 /**
-   \brief Base class used to represent trace objects.
-   These objects are used to trace the execution of different engines in Lean.
-   The traces may help users understanding why something did not work.
-   The traces are particularly important for the elaborator.
+   \brief Base class used to represent justification objects.
+   These objects are used to justification the execution of different engines in Lean.
+   The justifications may help users understanding why something did not work.
+   The justifications are particularly important for the elaborator.
 */
-class trace_cell {
+class justification_cell {
     MK_LEAN_RC();
     void dealloc() { delete this; }
 protected:
     static void add_pos_info(format & r, expr const & e, pos_info_provider const * p);
 public:
-    trace_cell():m_rc(0) {}
-    virtual ~trace_cell() {}
+    justification_cell():m_rc(0) {}
+    virtual ~justification_cell() {}
     virtual format pp_header(formatter const & fmt, options const & opts) const = 0;
     virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
-    virtual void get_children(buffer<trace_cell*> & r) const = 0;
+    virtual void get_children(buffer<justification_cell*> & r) const = 0;
     virtual expr const & get_main_expr() const { return expr::null(); }
     bool is_shared() const { return get_rc() > 1; }
 };
 
 /**
-   \brief Smart pointer for trace_cell's
+   \brief Smart pointer for justification_cell's
 */
-class trace {
-    trace_cell * m_ptr;
+class justification {
+    justification_cell * m_ptr;
 public:
-    trace():m_ptr(nullptr) {}
-    trace(trace_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    trace(trace const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    trace(trace && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-    ~trace() { if (m_ptr) m_ptr->dec_ref(); }
+    justification():m_ptr(nullptr) {}
+    justification(justification_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    justification(justification const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    justification(justification && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    ~justification() { if (m_ptr) m_ptr->dec_ref(); }
 
     operator bool() const { return m_ptr != nullptr; }
 
-    trace_cell * raw() const { return m_ptr; }
+    justification_cell * raw() const { return m_ptr; }
 
-    friend void swap(trace & a, trace & b) { std::swap(a.m_ptr, b.m_ptr); }
+    friend void swap(justification & a, justification & b) { std::swap(a.m_ptr, b.m_ptr); }
 
-    trace & operator=(trace const & s) { LEAN_COPY_REF(trace, s); }
-    trace & operator=(trace && s) { LEAN_MOVE_REF(trace, s); }
+    justification & operator=(justification const & s) { LEAN_COPY_REF(justification, s); }
+    justification & operator=(justification && s) { LEAN_MOVE_REF(justification, s); }
     format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const {
         lean_assert(m_ptr);
         return m_ptr->pp(fmt, opts, p, display_children);
     }
     expr const & get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : expr::null(); }
-    void get_children(buffer<trace_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
+    void get_children(buffer<justification_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
     bool has_children() const;
 };
 
@@ -70,5 +70,5 @@ public:
    \brief Return true iff \c t depends on \c d.
    That is \c t is a descendant of \c d.
 */
-bool depends_on(trace const & t, trace const & d);
+bool depends_on(justification const & t, justification const & d);
 }
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 57856c7c7..5af1f70e4 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -87,12 +87,12 @@ expr substitution::get_subst(expr const & m) const {
 static name g_unique_name = name::mk_internal_unique_name();
 
 void swap(metavar_env & a, metavar_env & b) {
-    swap(a.m_name_generator,   b.m_name_generator);
-    swap(a.m_substitution,     b.m_substitution);
-    swap(a.m_metavar_types,    b.m_metavar_types);
-    swap(a.m_metavar_contexts, b.m_metavar_contexts);
-    swap(a.m_metavar_traces,   b.m_metavar_traces);
-    std::swap(a.m_timestamp,   b.m_timestamp);
+    swap(a.m_name_generator,         b.m_name_generator);
+    swap(a.m_substitution,           b.m_substitution);
+    swap(a.m_metavar_types,          b.m_metavar_types);
+    swap(a.m_metavar_contexts,       b.m_metavar_contexts);
+    swap(a.m_metavar_justifications, b.m_metavar_justifications);
+    std::swap(a.m_timestamp,         b.m_timestamp);
 }
 
 void metavar_env::inc_timestamp() {
@@ -173,17 +173,17 @@ bool metavar_env::has_type(expr const & m) const {
 }
 
 
-trace metavar_env::get_trace(expr const & m) const {
+justification metavar_env::get_justification(expr const & m) const {
     lean_assert(is_metavar(m));
-    return get_trace(metavar_name(m));
+    return get_justification(metavar_name(m));
 }
 
-trace metavar_env::get_trace(name const & m) const {
-    auto e = const_cast<metavar_env*>(this)->m_metavar_traces.splay_find(m);
+justification metavar_env::get_justification(name const & m) const {
+    auto e = const_cast<metavar_env*>(this)->m_metavar_justifications.splay_find(m);
     if (e) {
         return e->second;
     } else {
-        return trace();
+        return justification();
     }
 }
 
@@ -196,18 +196,18 @@ bool metavar_env::is_assigned(expr const & m) const {
     return is_assigned(metavar_name(m));
 }
 
-void metavar_env::assign(name const & m, expr const & t, trace const & tr) {
+void metavar_env::assign(name const & m, expr const & t, justification const & j) {
     lean_assert(!is_assigned(m));
     inc_timestamp();
     m_substitution.assign(m, t);
-    if (tr)
-        m_metavar_traces.insert(m, tr);
+    if (j)
+        m_metavar_justifications.insert(m, j);
 }
 
-void metavar_env::assign(expr const & m, expr const & t, trace const & tr) {
+void metavar_env::assign(expr const & m, expr const & t, justification const & j) {
     lean_assert(is_metavar(m));
     lean_assert(!has_local_context(m));
-    assign(metavar_name(m), t, tr);
+    assign(metavar_name(m), t, j);
 }
 
 struct found_unassigned{};
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index 6ed469b23..d0f2e8330 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "util/name_generator.h"
 #include "kernel/expr.h"
 #include "kernel/context.h"
-#include "kernel/trace.h"
+#include "kernel/justification.h"
 
 namespace lean {
 /**
@@ -89,16 +89,16 @@ void swap(substitution & s1, substitution & s2);
    4- Collecting constraints
 */
 class metavar_env {
-    typedef splay_map<name, expr, name_cmp>    name2expr;
-    typedef splay_map<name, context, name_cmp> name2context;
-    typedef splay_map<name, trace, name_cmp>   name2trace;
+    typedef splay_map<name, expr, name_cmp>          name2expr;
+    typedef splay_map<name, context, name_cmp>       name2context;
+    typedef splay_map<name, justification, name_cmp> name2justification;
 
-    name_generator m_name_generator;
-    substitution   m_substitution;
-    name2expr      m_metavar_types;
-    name2context   m_metavar_contexts;
-    name2trace     m_metavar_traces;
-    unsigned       m_timestamp;
+    name_generator     m_name_generator;
+    substitution       m_substitution;
+    name2expr          m_metavar_types;
+    name2context       m_metavar_contexts;
+    name2justification m_metavar_justifications;
+    unsigned           m_timestamp;
 
     void inc_timestamp();
 public:
@@ -146,12 +146,12 @@ public:
     bool has_type(name const & m) const;
 
     /**
-       \brief Return the trace/justification for an assigned metavariable.
+       \brief Return the justification for an assigned metavariable.
        \pre is_metavar(m)
        \pre is_assigned(m)
     */
-    trace get_trace(expr const & m) const;
-    trace get_trace(name const & m) const;
+    justification get_justification(expr const & m) const;
+    justification get_justification(name const & m) const;
 
 
     /**
@@ -172,7 +172,7 @@ public:
 
        \pre !is_assigned(m)
     */
-    void assign(name const & m, expr const & t, trace const & tr = trace());
+    void assign(name const & m, expr const & t, justification const & j = justification());
 
     /**
        \brief Assign metavariable \c m to \c t.
@@ -181,7 +181,7 @@ public:
        \pre !has_meta_context(m)
        \pre !is_assigned(m)
     */
-    void assign(expr const & m, expr const & t, trace const & tr = trace());
+    void assign(expr const & m, expr const & t, justification const & j = justification());
 
     /**
        \brief Return the set of substitutions.
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 074558bd7..bf329b54a 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/builtin.h"
 #include "kernel/free_vars.h"
-#include "kernel/type_checker_trace.h"
+#include "kernel/type_checker_justification.h"
 
 namespace lean {
 static name g_x_name("x");
@@ -55,8 +55,8 @@ class type_checker::imp {
             expr A   = m_menv->mk_metavar(ctx);
             expr B   = m_menv->mk_metavar(ctx);
             expr p   = mk_pi(g_x_name, A, B(Var(0)));
-            trace tr = mk_function_expected_trace(ctx, s);
-            m_uc->push_back(mk_eq_constraint(ctx, r, p, tr));
+            justification jst = mk_function_expected_justification(ctx, s);
+            m_uc->push_back(mk_eq_constraint(ctx, r, p, jst));
             return p;
         }
         throw function_expected_exception(m_env, ctx, s);
@@ -73,8 +73,8 @@ class type_checker::imp {
         if (u == Bool)
             return Type();
         if (has_metavar(u) && m_menv) {
-            trace tr = mk_type_expected_trace(ctx, s);
-            m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, tr));
+            justification jst = mk_type_expected_justification(ctx, s);
+            m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
             return u;
         }
         throw type_expected_exception(m_env, ctx, s);
@@ -123,8 +123,8 @@ class type_checker::imp {
             while (true) {
                 expr const & c   = arg(e, i);
                 expr const & c_t = arg_types[i];
-                auto mk_trace = [&](){ return mk_app_type_match_trace(ctx, e, i); }; // thunk for creating trace object if needed
-                if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_trace))
+                auto mk_justification = [&](){ return mk_app_type_match_justification(ctx, e, i); }; // thunk for creating justification object if needed
+                if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_justification))
                     throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data());
                 if (closed(abst_body(f_t)))
                     f_t = abst_body(f_t);
@@ -169,9 +169,9 @@ class type_checker::imp {
                 r = mk_type(max(ty_level(t1), ty_level(t2)));
             } else {
                 lean_assert(m_uc);
-                trace tr = mk_max_type_trace(ctx, e);
+                justification jst = mk_max_type_justification(ctx, e);
                 r = m_menv->mk_metavar(ctx);
-                m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, tr));
+                m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, jst));
             }
             break;
         }
@@ -180,8 +180,8 @@ class type_checker::imp {
             if (let_type(e)) {
                 expr ty = infer_type_core(let_type(e), ctx);
                 check_type(ty, let_type(e), ctx); // check if it is really a type
-                auto mk_trace = [&](){ return mk_def_type_match_trace(ctx, let_name(e), let_value(e)); }; // thunk for creating trace object if needed
-                if (!is_convertible(lt, let_type(e), ctx, mk_trace))
+                auto mk_justification = [&](){ return mk_def_type_match_justification(ctx, let_name(e), let_value(e)); }; // thunk for creating justification object if needed
+                if (!is_convertible(lt, let_type(e), ctx, mk_justification))
                     throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt);
             }
             {
@@ -235,8 +235,8 @@ class type_checker::imp {
         }
     }
 
-    template<typename MkTrace>
-    bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkTrace const & mk_trace) {
+    template<typename MkJustification>
+    bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkJustification const & mk_justification) {
         if (is_convertible_core(given, expected))
             return true;
         expr new_given    = normalize(given, ctx);
@@ -244,7 +244,7 @@ class type_checker::imp {
         if (is_convertible_core(new_given, new_expected))
             return true;
         if (m_menv && (has_metavar(new_given) || has_metavar(new_expected))) {
-            m_uc->push_back(mk_convertible_constraint(ctx, new_given, new_expected, mk_trace()));
+            m_uc->push_back(mk_convertible_constraint(ctx, new_given, new_expected, mk_justification()));
             return true;
         }
         return false;
@@ -292,8 +292,8 @@ public:
     bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
         set_ctx(ctx);
         set_menv(nullptr);
-        auto mk_trace = [](){ lean_unreachable(); return trace(); };
-        return is_convertible(t1, t2, ctx, mk_trace);
+        auto mk_justification = [](){ lean_unreachable(); return justification(); };
+        return is_convertible(t1, t2, ctx, mk_justification);
     }
 
     void check_type(expr const & e, context const & ctx) {
diff --git a/src/kernel/type_checker_trace.cpp b/src/kernel/type_checker_justification.cpp
similarity index 50%
rename from src/kernel/type_checker_trace.cpp
rename to src/kernel/type_checker_justification.cpp
index b23acf9da..e9529e67d 100644
--- a/src/kernel/type_checker_trace.cpp
+++ b/src/kernel/type_checker_justification.cpp
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/type_checker_trace.h"
+#include "kernel/type_checker_justification.h"
 
 namespace lean {
 
-function_expected_trace_cell::~function_expected_trace_cell() {
+function_expected_justification_cell::~function_expected_justification_cell() {
 }
 
-format function_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
+format function_expected_justification_cell::pp_header(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_app, false, opts);
     format r;
@@ -20,17 +20,17 @@ format function_expected_trace_cell::pp_header(formatter const & fmt, options co
     return r;
 }
 
-void function_expected_trace_cell::get_children(buffer<trace_cell*> &) const {
+void function_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
 }
 
-expr const & function_expected_trace_cell::get_main_expr() const {
+expr const & function_expected_justification_cell::get_main_expr() const {
     return m_app;
 }
 
-app_type_match_trace_cell::~app_type_match_trace_cell() {
+app_type_match_justification_cell::~app_type_match_justification_cell() {
 }
 
-format app_type_match_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
+format app_type_match_justification_cell::pp_header(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
     format r;
     r += format("Type of argument ");
@@ -48,17 +48,17 @@ format app_type_match_trace_cell::pp_header(formatter const & fmt, options const
     return r;
 }
 
-void app_type_match_trace_cell::get_children(buffer<trace_cell*> &) const {
+void app_type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
 }
 
-expr const & app_type_match_trace_cell::get_main_expr() const {
+expr const & app_type_match_justification_cell::get_main_expr() const {
     return m_app;
 }
 
-type_expected_trace_cell::~type_expected_trace_cell() {
+type_expected_justification_cell::~type_expected_justification_cell() {
 }
 
-format type_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
+format type_expected_justification_cell::pp_header(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_type, false, opts);
     format r;
@@ -67,17 +67,17 @@ format type_expected_trace_cell::pp_header(formatter const & fmt, options const
     return r;
 }
 
-void type_expected_trace_cell::get_children(buffer<trace_cell*> &) const {
+void type_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
 }
 
-expr const & type_expected_trace_cell::get_main_expr() const {
+expr const & type_expected_justification_cell::get_main_expr() const {
     return m_type;
 }
 
-def_type_match_trace_cell::~def_type_match_trace_cell() {
+def_type_match_justification_cell::~def_type_match_justification_cell() {
 }
 
-format def_type_match_trace_cell::pp_header(formatter const &, options const &) const {
+format def_type_match_justification_cell::pp_header(formatter const &, options const &) const {
     format r;
     r += format("Type of definition '");
     r += format(get_name());
@@ -85,10 +85,10 @@ format def_type_match_trace_cell::pp_header(formatter const &, options const &)
     return r;
 }
 
-void def_type_match_trace_cell::get_children(buffer<trace_cell*> &) const {
+void def_type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
 }
 
-expr const & def_type_match_trace_cell::get_main_expr() const {
+expr const & def_type_match_justification_cell::get_main_expr() const {
     return m_value;
 }
 }
diff --git a/src/kernel/type_checker_justification.h b/src/kernel/type_checker_justification.h
new file mode 100644
index 000000000..fb90937e5
--- /dev/null
+++ b/src/kernel/type_checker_justification.h
@@ -0,0 +1,128 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/justification.h"
+#include "kernel/expr.h"
+#include "kernel/context.h"
+
+namespace lean {
+/**
+   \brief Justification produced by the type checker when the application \c m_app
+   is an application <tt>(f ...)</tt>, the type \c T of \c f contains metavariables, and
+   it is not clear whether it is a Pi or not. In this case, the type checker adds
+   the constraint
+
+       <tt>ctx |- T == Pi (x : ?A), ?B x</tt>
+
+   where, \c ?A and \c ?B are fresh metavariables.
+   This justification cell is used to justify the new constraint.
+*/
+class function_expected_justification_cell : public justification_cell {
+    context m_ctx;
+    expr    m_app;
+public:
+    function_expected_justification_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
+    virtual ~function_expected_justification_cell();
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
+    virtual void get_children(buffer<justification_cell*> &) const;
+    virtual expr const & get_main_expr() const;
+    context const & get_context() const { return m_ctx; }
+    expr const & get_app() const { return m_app; }
+};
+
+/**
+   \brief Justification produced by the type checker for application argument type matching.
+   When checking an application <tt>(f a_1 ... a_i ...)</tt>, the type
+   \c T_inferred of \c a_i must be convertible to the expected type \c T_expected.  If
+   \c T_expected or \c T_inferred contain metavariables, and it is not clear whether
+   \c T_inferred is convertible to \c T_expected, then the type checker adds the constraint
+
+      <tt>ctx |- T_inferred << T_expected</tt>
+
+   This justification cell is used to justify this constraint.
+*/
+class app_type_match_justification_cell : public justification_cell {
+    context  m_ctx;
+    expr     m_app;
+    unsigned m_i;
+public:
+    app_type_match_justification_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {}
+    virtual ~app_type_match_justification_cell();
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
+    virtual void get_children(buffer<justification_cell*> &) const;
+    virtual expr const & get_main_expr() const;
+    context const & get_context() const { return m_ctx; }
+    expr const & get_app() const { return m_app; }
+    unsigned get_arg_pos() const { return m_i; }
+};
+
+/**
+   \brief Justification produced by the type checker when the type \c T of \c type must be of the form
+   <tt>Type l</tt>, and \c T constains metavariables, and it is not of this form.
+   The type checker adds the following constraint
+
+      <tt>ctx |- T << Type U</tt>
+
+   This justification cell is used to justify these constraints.
+*/
+class type_expected_justification_cell : public justification_cell {
+    context m_ctx;
+    expr    m_type;
+public:
+    type_expected_justification_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {}
+    virtual ~type_expected_justification_cell();
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
+    virtual void get_children(buffer<justification_cell*> &) const;
+    virtual expr const & get_main_expr() const;
+    context const & get_context() const { return m_ctx; }
+    expr const & get_type() const { return m_type; }
+};
+
+/**
+   \brief If \c type is of the form <tt>Pi x : A, B</tt>, where \c A has type \c T1 and \c B has type \c T2,
+   and \c T1 or \c T2 have metavariables, then the type checker adds the following constraint
+
+     <tt>ctx |- max(T1, T2) == ?T
+
+   where ?T is a new metavariable, and this justification cell is used to justify the new constraint.
+*/
+class max_type_justification_cell : public type_expected_justification_cell {
+public:
+    max_type_justification_cell(context const & c, expr const & t):type_expected_justification_cell(c, t) {}
+};
+
+/**
+   \brief Justification produced by the type checker when checking whether the type \c T_inferred of \c value
+   is convertible to the expected type \c T_expected. If \c T_expected or \c T_inferred contain
+   metavariables, and it is not clear whether \c T_inferred is convertible to \c T_expected,
+   then the type checker adds the constraint
+
+      <tt>ctx |- T_inferred << T_expected</tt>
+
+   This justification cell is used to justify this constraint.
+*/
+class def_type_match_justification_cell : public justification_cell {
+    context m_ctx;
+    name    m_name;
+    expr    m_value;
+public:
+    def_type_match_justification_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {}
+    virtual ~def_type_match_justification_cell();
+    virtual format pp_header(formatter const & fmt, options const & opts) const;
+    virtual void get_children(buffer<justification_cell*> &) const;
+    virtual expr const & get_main_expr() const;
+    context const & get_context() const { return m_ctx; }
+    name const & get_name() const { return m_name; }
+    expr const & get_value() const { return m_value; }
+};
+
+inline justification mk_function_expected_justification(context const & ctx, expr const & app) { return justification(new function_expected_justification_cell(ctx, app)); }
+inline justification mk_app_type_match_justification(context const & ctx, expr const & app, unsigned i) { return justification(new app_type_match_justification_cell(ctx, app, i)); }
+inline justification mk_type_expected_justification(context const & ctx, expr const & type) { return justification(new type_expected_justification_cell(ctx, type)); }
+inline justification mk_max_type_justification(context const & ctx, expr const & type) { return justification(new max_type_justification_cell(ctx, type)); }
+inline justification mk_def_type_match_justification(context const & ctx, name const & n, expr const & v) { return justification(new def_type_match_justification_cell(ctx, n, v)); }
+}
diff --git a/src/kernel/type_checker_trace.h b/src/kernel/type_checker_trace.h
deleted file mode 100644
index 0dcdcc864..000000000
--- a/src/kernel/type_checker_trace.h
+++ /dev/null
@@ -1,128 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/trace.h"
-#include "kernel/expr.h"
-#include "kernel/context.h"
-
-namespace lean {
-/**
-   \brief Trace produced by the type checker when the application \c m_app
-   is an application <tt>(f ...)</tt>, the type \c T of \c f contains metavariables, and
-   it is not clear whether it is a Pi or not. In this case, the type checker adds
-   the constraint
-
-       <tt>ctx |- T == Pi (x : ?A), ?B x</tt>
-
-   where, \c ?A and \c ?B are fresh metavariables.
-   This trace cell is used to justify/trace the new constraint.
-*/
-class function_expected_trace_cell : public trace_cell {
-    context m_ctx;
-    expr    m_app;
-public:
-    function_expected_trace_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
-    virtual ~function_expected_trace_cell();
-    virtual format pp_header(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace_cell*> &) const;
-    virtual expr const & get_main_expr() const;
-    context const & get_context() const { return m_ctx; }
-    expr const & get_app() const { return m_app; }
-};
-
-/**
-   \brief Trace produced by the type checker for application argument type matching.
-   When checking an application <tt>(f a_1 ... a_i ...)</tt>, the type
-   \c T_inferred of \c a_i must be convertible to the expected type \c T_expected.  If
-   \c T_expected or \c T_inferred contain metavariables, and it is not clear whether
-   \c T_inferred is convertible to \c T_expected, then the type checker adds the constraint
-
-      <tt>ctx |- T_inferred << T_expected</tt>
-
-   This trace cell is used to justify this constraint.
-*/
-class app_type_match_trace_cell : public trace_cell {
-    context  m_ctx;
-    expr     m_app;
-    unsigned m_i;
-public:
-    app_type_match_trace_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {}
-    virtual ~app_type_match_trace_cell();
-    virtual format pp_header(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace_cell*> &) const;
-    virtual expr const & get_main_expr() const;
-    context const & get_context() const { return m_ctx; }
-    expr const & get_app() const { return m_app; }
-    unsigned get_arg_pos() const { return m_i; }
-};
-
-/**
-   \brief Trace produced by the type checker when the type \c T of \c type must be of the form
-   <tt>Type l</tt>, and \c T constains metavariables, and it is not of this form.
-   The type checker adds the following constraint
-
-      <tt>ctx |- T << Type U</tt>
-
-   This trace cell is used to justify these constraints.
-*/
-class type_expected_trace_cell : public trace_cell {
-    context m_ctx;
-    expr    m_type;
-public:
-    type_expected_trace_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {}
-    virtual ~type_expected_trace_cell();
-    virtual format pp_header(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace_cell*> &) const;
-    virtual expr const & get_main_expr() const;
-    context const & get_context() const { return m_ctx; }
-    expr const & get_type() const { return m_type; }
-};
-
-/**
-   \brief If \c type is of the form <tt>Pi x : A, B</tt>, where \c A has type \c T1 and \c B has type \c T2,
-   and \c T1 or \c T2 have metavariables, then the type checker adds the following constraint
-
-     <tt>ctx |- max(T1, T2) == ?T
-
-   where ?T is a new metavariable, and this trace cell is used to justify the new constraint.
-*/
-class max_type_trace_cell : public type_expected_trace_cell {
-public:
-    max_type_trace_cell(context const & c, expr const & t):type_expected_trace_cell(c, t) {}
-};
-
-/**
-   \brief Trace produced by the type checker when checking whether the type \c T_inferred of \c value
-   is convertible to the expected type \c T_expected. If \c T_expected or \c T_inferred contain
-   metavariables, and it is not clear whether \c T_inferred is convertible to \c T_expected,
-   then the type checker adds the constraint
-
-      <tt>ctx |- T_inferred << T_expected</tt>
-
-   This trace cell is used to justify this constraint.
-*/
-class def_type_match_trace_cell : public trace_cell {
-    context m_ctx;
-    name    m_name;
-    expr    m_value;
-public:
-    def_type_match_trace_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {}
-    virtual ~def_type_match_trace_cell();
-    virtual format pp_header(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace_cell*> &) const;
-    virtual expr const & get_main_expr() const;
-    context const & get_context() const { return m_ctx; }
-    name const & get_name() const { return m_name; }
-    expr const & get_value() const { return m_value; }
-};
-
-inline trace mk_function_expected_trace(context const & ctx, expr const & app) { return trace(new function_expected_trace_cell(ctx, app)); }
-inline trace mk_app_type_match_trace(context const & ctx, expr const & app, unsigned i) { return trace(new app_type_match_trace_cell(ctx, app, i)); }
-inline trace mk_type_expected_trace(context const & ctx, expr const & type) { return trace(new type_expected_trace_cell(ctx, type)); }
-inline trace mk_max_type_trace(context const & ctx, expr const & type) { return trace(new max_type_trace_cell(ctx, type)); }
-inline trace mk_def_type_match_trace(context const & ctx, name const & n, expr const & v) { return trace(new def_type_match_trace_cell(ctx, n, v)); }
-}
diff --git a/src/kernel/unification_constraint.cpp b/src/kernel/unification_constraint.cpp
index 2c137c5d1..432111ffc 100644
--- a/src/kernel/unification_constraint.cpp
+++ b/src/kernel/unification_constraint.cpp
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #include "kernel/unification_constraint.h"
 
 namespace lean {
-unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t):
-    m_kind(k), m_ctx(c), m_trace(t), m_rc(1) {
+unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j):
+    m_kind(k), m_ctx(c), m_justification(j), m_rc(1) {
 }
 unification_constraint_cell::~unification_constraint_cell() {
 }
@@ -23,10 +23,10 @@ static format add_context(formatter const & fmt, options const & opts, context c
     return group(format{ctx_fmt, space(), turnstile, line(), body});
 }
 
-static format add_trace(formatter const & fmt, options const & opts, format const & body, trace const & tr, pos_info_provider const * p, bool include_trace) {
-    if (tr && include_trace) {
+static format add_justification(formatter const & fmt, options const & opts, format const & body, justification const & jst, pos_info_provider const * p, bool include_justification) {
+    if (jst && include_justification) {
         unsigned indent  = get_pp_indent(opts);
-        return format{body, line(), format("Trace:"), nest(indent, compose(line(), tr.pp(fmt, opts, p)))};
+        return format{body, line(), format("Justification:"), nest(indent, compose(line(), jst.pp(fmt, opts, p)))};
     } else {
         return body;
     }
@@ -43,8 +43,8 @@ static format mk_unification_op(options const & opts) {
     return unicode ? format("\u2248") /* ≈ */ : format("=?=");
 }
 
-unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t):
-    unification_constraint_cell(unification_constraint_kind::Eq, c, t),
+unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j):
+    unification_constraint_cell(unification_constraint_kind::Eq, c, j),
     m_lhs(lhs),
     m_rhs(rhs) {
 }
@@ -52,15 +52,15 @@ unification_constraint_eq::unification_constraint_eq(context const & c, expr con
 unification_constraint_eq::~unification_constraint_eq() {
 }
 
-format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
+format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
     format op   = mk_unification_op(opts);
     format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op);
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, p, include_trace);
+    return add_justification(fmt, opts, body, m_justification, p, include_justification);
 }
 
-unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t):
-    unification_constraint_cell(unification_constraint_kind::Convertible, c, t),
+unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j):
+    unification_constraint_cell(unification_constraint_kind::Convertible, c, j),
     m_from(from),
     m_to(to) {
 }
@@ -68,16 +68,16 @@ unification_constraint_convertible::unification_constraint_convertible(context c
 unification_constraint_convertible::~unification_constraint_convertible() {
 }
 
-format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
+format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
     bool unicode = get_pp_unicode(opts);
     format op    = unicode ? format("\u227A") /* ≺ */ : format("<<");
     format body  = mk_binary(fmt, opts, m_ctx, m_from, m_to, op);
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, p, include_trace);
+    return add_justification(fmt, opts, body, m_justification, p, include_justification);
 }
 
-unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t):
-    unification_constraint_cell(unification_constraint_kind::Max, c, t),
+unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j):
+    unification_constraint_cell(unification_constraint_kind::Max, c, j),
     m_lhs1(lhs1),
     m_lhs2(lhs2),
     m_rhs(rhs) {
@@ -86,18 +86,18 @@ unification_constraint_max::unification_constraint_max(context const & c, expr c
 unification_constraint_max::~unification_constraint_max() {
 }
 
-format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
+format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
     format op       = mk_unification_op(opts);
     format lhs1_fmt = fmt(m_ctx, m_lhs1, false, opts);
     format lhs2_fmt = fmt(m_ctx, m_lhs2, false, opts);
     format rhs_fmt  = fmt(m_ctx, m_rhs, false, opts);
     format body     = group(format{format("max"), lp(), lhs1_fmt, comma(), nest(4, compose(line(), lhs2_fmt)), rp(), space(), op, line(), rhs_fmt});
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, p, include_trace);
+    return add_justification(fmt, opts, body, m_justification, p, include_justification);
 }
 
-unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t):
-    unification_constraint_cell(unification_constraint_kind::Choice, c, t),
+unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, justification const & j):
+    unification_constraint_cell(unification_constraint_kind::Choice, c, j),
     m_mvar(mvar),
     m_num_choices(num) {
 }
@@ -105,7 +105,7 @@ unification_constraint_choice::unification_constraint_choice(context const & c,
 unification_constraint_choice::~unification_constraint_choice() {
 }
 
-format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
+format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
     bool unicode    = get_pp_unicode(opts);
     format m_fmt    = fmt(m_ctx, m_mvar, false, opts);
     format eq_op    = mk_unification_op(opts);
@@ -118,31 +118,31 @@ format unification_constraint_choice::pp(formatter const & fmt, options const &
     }
     body = group(body);
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, p, include_trace);
+    return add_justification(fmt, opts, body, m_justification, p, include_justification);
 }
 
-unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t) {
-    return unification_constraint(new unification_constraint_eq(c, lhs, rhs, t));
+unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j) {
+    return unification_constraint(new unification_constraint_eq(c, lhs, rhs, j));
 }
 
-unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t) {
-    return unification_constraint(new unification_constraint_convertible(c, from, to, t));
+unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j) {
+    return unification_constraint(new unification_constraint_convertible(c, from, to, j));
 }
 
-unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t) {
-    return unification_constraint(new unification_constraint_max(c, lhs1, lhs2, rhs, t));
+unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j) {
+    return unification_constraint(new unification_constraint_max(c, lhs1, lhs2, rhs, j));
 }
 
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t) {
+unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j) {
     char * mem   = new char[sizeof(unification_constraint_choice) + num*sizeof(expr)];
-    unification_constraint r(new (mem) unification_constraint_choice(c, mvar, num, t));
+    unification_constraint r(new (mem) unification_constraint_choice(c, mvar, num, j));
     expr * m_choices = to_choice(r)->m_choices;
     for (unsigned i = 0; i < num; i++)
         new (m_choices+i) expr(choices[i]);
     return r;
 }
 
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, trace const & t) {
-    return mk_choice_constraint(c, mvar, choices.size(), choices.begin(), t);
+unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, justification const & j) {
+    return mk_choice_constraint(c, mvar, choices.size(), choices.begin(), j);
 }
 }
diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h
index acdad3302..34d22d6c0 100644
--- a/src/kernel/unification_constraint.h
+++ b/src/kernel/unification_constraint.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include "kernel/expr.h"
 #include "kernel/context.h"
-#include "kernel/trace.h"
+#include "kernel/justification.h"
 
 namespace lean {
 /**
@@ -37,17 +37,17 @@ class unification_constraint_cell {
 protected:
     unification_constraint_kind m_kind;
     context                     m_ctx;
-    trace                       m_trace; //!< justification for this constraint
+    justification               m_justification; //!< justification for this constraint
     MK_LEAN_RC();
     void dealloc();
 public:
-    unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t);
+    unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j);
     virtual ~unification_constraint_cell();
     unification_constraint_kind kind() const { return m_kind; }
-    trace const & get_trace() const { return m_trace; }
+    justification const & get_justification() const { return m_justification; }
     context const & get_context() const { return m_ctx; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const = 0;
-    void set_trace(trace const & t) { lean_assert(!m_trace); m_trace = t; }
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const = 0;
+    void set_justification(justification const & j) { lean_assert(!m_justification); m_justification = j; }
 };
 
 class unification_constraint {
@@ -70,18 +70,18 @@ public:
 
     operator bool() const { return m_ptr != nullptr; }
 
-    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_trace = false) const {
+    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const {
         lean_assert(m_ptr);
-        return m_ptr->pp(fmt, opts, p, include_trace);
+        return m_ptr->pp(fmt, opts, p, include_justification);
     }
 
-    trace const & get_trace() const { lean_assert(m_ptr); return m_ptr->get_trace(); }
-    void set_trace(trace const & t) { lean_assert(!get_trace()); lean_assert(m_ptr); m_ptr->set_trace(t); }
+    justification const & get_justification() const { lean_assert(m_ptr); return m_ptr->get_justification(); }
+    void set_justification(justification const & j) { lean_assert(!get_justification()); lean_assert(m_ptr); m_ptr->set_justification(j); }
 
-    friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
-    friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t);
-    friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
-    friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t);
+    friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j);
+    friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j);
+    friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
+    friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
 };
 
 /**
@@ -91,11 +91,11 @@ class unification_constraint_eq : public unification_constraint_cell {
     expr m_lhs;
     expr m_rhs;
 public:
-    unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t);
+    unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j);
     virtual ~unification_constraint_eq();
     expr const & get_lhs() const { return m_lhs; }
     expr const & get_rhs() const { return m_rhs; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
 };
 
 /**
@@ -107,11 +107,11 @@ class unification_constraint_convertible : public unification_constraint_cell {
     expr m_from;
     expr m_to;
 public:
-    unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t);
+    unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j);
     virtual ~unification_constraint_convertible();
     expr const & get_from() const { return m_from; }
     expr const & get_to() const   { return m_to; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
 };
 
 /**
@@ -122,12 +122,12 @@ class unification_constraint_max : public unification_constraint_cell {
     expr m_lhs2;
     expr m_rhs;
 public:
-    unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
+    unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
     virtual ~unification_constraint_max();
     expr const & get_lhs1() const { return m_lhs1; }
     expr const & get_lhs2() const { return m_lhs2; }
     expr const & get_rhs() const  { return m_rhs; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
 };
 
 /**
@@ -137,23 +137,23 @@ class unification_constraint_choice : public unification_constraint_cell {
     expr     m_mvar;
     unsigned m_num_choices;
     expr     m_choices[0];
-    friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t);
+    friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
 public:
-    unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t);
+    unification_constraint_choice(context const & c, expr const & mvar, unsigned num, justification const & j);
     virtual ~unification_constraint_choice();
     expr const & get_mvar() const               { return m_mvar; }
     unsigned     get_num_choices() const        { return m_num_choices; }
     expr const & get_choice(unsigned idx) const { lean_assert(idx < m_num_choices); return m_choices[idx]; }
     expr const * begin_choices() const          { return m_choices; }
     expr const * end_choices() const            { return m_choices + m_num_choices; }
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
 };
 
-unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
-unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t);
-unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t);
-unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, trace const & t);
+unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j);
+unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j);
+unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
+unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
+unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, justification const & j);
 
 inline bool is_eq(unification_constraint const & c)          { return c.kind() == unification_constraint_kind::Eq; }
 inline bool is_convertible(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Convertible; }
@@ -166,7 +166,7 @@ inline unification_constraint_max *         to_max(unification_constraint const
 inline unification_constraint_choice *      to_choice(unification_constraint const & c)      { lean_assert(is_choice(c)); return static_cast<unification_constraint_choice*>(c.raw()); }
 
 inline context const & get_context(unification_constraint const & c) { return c.raw()->get_context(); }
-inline trace   const & get_trace(unification_constraint const & c) { return c.raw()->get_trace(); }
+inline justification   const & get_justification(unification_constraint const & c) { return c.raw()->get_justification(); }
 inline expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); }
 inline expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); }
 inline expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); }
diff --git a/src/library/elaborator/CMakeLists.txt b/src/library/elaborator/CMakeLists.txt
index cf1d33dd8..d6854a25c 100644
--- a/src/library/elaborator/CMakeLists.txt
+++ b/src/library/elaborator/CMakeLists.txt
@@ -1,2 +1,2 @@
-add_library(elaborator elaborator.cpp elaborator_trace.cpp)
+add_library(elaborator elaborator.cpp elaborator_justification.cpp)
 target_link_libraries(elaborator ${LEAN_LIBS})
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 0c581530b..1449f063d 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 #include "library/update_expr.h"
 #include "library/reduce.h"
 #include "library/elaborator/elaborator.h"
-#include "library/elaborator/elaborator_trace.h"
+#include "library/elaborator/elaborator_justification.h"
 
 namespace lean {
 static name g_x_name("x");
@@ -46,9 +46,9 @@ class elaborator::imp {
        \brief Base class for case splits performed by the elaborator.
     */
     struct case_split {
-        trace              m_curr_assumption; // trace object used to justify current split
-        state              m_prev_state;
-        std::vector<trace> m_failed_traces;   // traces/justifications for failed branches
+        justification              m_curr_assumption; // object used to justify current split
+        state                      m_prev_state;
+        std::vector<justification> m_failed_justifications; // justifications for failed branches
 
         case_split(state const & prev_state):m_prev_state(prev_state) {}
         virtual ~case_split() {}
@@ -80,10 +80,10 @@ class elaborator::imp {
        \brief General purpose case split object
     */
     struct generic_case_split : public case_split {
-        unification_constraint m_constraint;
-        unsigned               m_idx;    // current alternative
-        std::vector<state>     m_states; // alternatives
-        std::vector<trace>     m_assumptions; // assumption for each alternative
+        unification_constraint     m_constraint;
+        unsigned                   m_idx;    // current alternative
+        std::vector<state>         m_states; // alternatives
+        std::vector<justification> m_assumptions; // assumption for each alternative
 
         generic_case_split(unification_constraint const & cnstr, state const & prev_state):
             case_split(prev_state),
@@ -97,7 +97,7 @@ class elaborator::imp {
             return owner.next_generic_case(*this);
         }
 
-        void push_back(state const & s, trace const & tr) {
+        void push_back(state const & s, justification const & tr) {
             m_states.push_back(s);
             m_assumptions.push_back(tr);
         }
@@ -142,28 +142,28 @@ class elaborator::imp {
     std::shared_ptr<elaborator_plugin>       m_plugin;
     unsigned                                 m_next_id;
     int                                      m_quota;
-    trace                                    m_conflict;
+    justification                            m_conflict;
     bool                                     m_first;
     bool                                     m_interrupted;
 
 
     // options
-    bool                                     m_use_traces;
+    bool                                     m_use_justifications;
     bool                                     m_use_normalizer;
 
     void set_options(options const &) {
-        m_use_traces     = true;
-        m_use_normalizer = true;
+        m_use_justifications = true;
+        m_use_normalizer     = true;
     }
 
     void reset_quota() {
         m_quota = m_state.m_queue.size();
     }
 
-    trace mk_assumption() {
+    justification mk_assumption() {
         unsigned id = m_next_id;
         m_next_id++;
-        return trace(new assumption_trace(id));
+        return justification(new assumption_justification(id));
     }
 
     /** \brief Add given constraint to the front of the current constraint queue */
@@ -190,11 +190,11 @@ class elaborator::imp {
         return m_state.m_menv.get_subst(m);
     }
 
-    /** \brief Return the trace/justification for an assigned metavariable */
-    trace get_mvar_trace(expr const & m) const {
+    /** \brief Return the justification/justification for an assigned metavariable */
+    justification get_mvar_justification(expr const & m) const {
         lean_assert(is_metavar(m));
         lean_assert(is_assigned(m));
-        return m_state.m_menv.get_trace(m);
+        return m_state.m_menv.get_justification(m);
     }
 
     /** \brief Return the type of an metavariable */
@@ -286,59 +286,59 @@ class elaborator::imp {
        \brief Auxiliary method for pushing a new constraint to the given constraint queue.
        If \c is_eq is true, then a equality constraint is created, otherwise a convertability constraint is created.
     */
-    void push_new_constraint(cnstr_queue & q, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, trace const & new_tr) {
+    void push_new_constraint(cnstr_queue & q, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
         if (is_eq)
-            q.push_front(mk_eq_constraint(new_ctx, new_a, new_b, new_tr));
+            q.push_front(mk_eq_constraint(new_ctx, new_a, new_b, new_jst));
         else
-            q.push_front(mk_convertible_constraint(new_ctx, new_a, new_b, new_tr));
+            q.push_front(mk_convertible_constraint(new_ctx, new_a, new_b, new_jst));
     }
 
-    void push_new_eq_constraint(cnstr_queue & q, context const & new_ctx, expr const & new_a, expr const & new_b, trace const & new_tr) {
-        push_new_constraint(q, true, new_ctx, new_a, new_b, new_tr);
+    void push_new_eq_constraint(cnstr_queue & q, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
+        push_new_constraint(q, true, new_ctx, new_a, new_b, new_jst);
     }
 
     /**
        \brief Auxiliary method for pushing a new constraint to the current constraint queue.
        If \c is_eq is true, then a equality constraint is created, otherwise a convertability constraint is created.
     */
-    void push_new_constraint(bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, trace const & new_tr) {
+    void push_new_constraint(bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
         reset_quota();
-        push_new_constraint(m_state.m_queue, is_eq, new_ctx, new_a, new_b, new_tr);
+        push_new_constraint(m_state.m_queue, is_eq, new_ctx, new_a, new_b, new_jst);
     }
 
     /**
        \brief Auxiliary method for pushing a new constraint to the current constraint queue.
        The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint.
-       The update is justified by \c new_tr.
+       The update is justified by \c new_jst.
     */
-    void push_updated_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b, trace const & new_tr) {
+    void push_updated_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b, justification const & new_jst) {
         lean_assert(is_eq(c) || is_convertible(c));
         context const & ctx = get_context(c);
         if (is_eq(c))
-            push_front(mk_eq_constraint(ctx, new_a, new_b, new_tr));
+            push_front(mk_eq_constraint(ctx, new_a, new_b, new_jst));
         else
-            push_front(mk_convertible_constraint(ctx, new_a, new_b, new_tr));
+            push_front(mk_convertible_constraint(ctx, new_a, new_b, new_jst));
     }
 
     /**
        \brief Auxiliary method for pushing a new constraint to the current constraint queue.
        The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint.
        The flag \c is_lhs says if the left-hand-side or right-hand-side are being updated with \c new_a.
-       The update is justified by \c new_tr.
+       The update is justified by \c new_jst.
     */
-    void push_updated_constraint(unification_constraint const & c, bool is_lhs, expr const & new_a, trace const & new_tr) {
+    void push_updated_constraint(unification_constraint const & c, bool is_lhs, expr const & new_a, justification const & new_jst) {
         lean_assert(is_eq(c) || is_convertible(c));
         context const & ctx = get_context(c);
         if (is_eq(c)) {
             if (is_lhs)
-                push_front(mk_eq_constraint(ctx, new_a, eq_rhs(c), new_tr));
+                push_front(mk_eq_constraint(ctx, new_a, eq_rhs(c), new_jst));
             else
-                push_front(mk_eq_constraint(ctx, eq_lhs(c), new_a, new_tr));
+                push_front(mk_eq_constraint(ctx, eq_lhs(c), new_a, new_jst));
         } else {
             if (is_lhs)
-                push_front(mk_convertible_constraint(ctx, new_a, convertible_to(c), new_tr));
+                push_front(mk_convertible_constraint(ctx, new_a, convertible_to(c), new_jst));
             else
-                push_front(mk_convertible_constraint(ctx, convertible_from(c), new_a, new_tr));
+                push_front(mk_convertible_constraint(ctx, convertible_from(c), new_a, new_jst));
         }
     }
 
@@ -347,13 +347,13 @@ class elaborator::imp {
        The new constraint is obtained from \c c by one or more normalization steps that produce \c new_a and \c new_b
     */
     void push_normalized_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b) {
-        push_updated_constraint(c, new_a, new_b, trace(new normalize_trace(c)));
+        push_updated_constraint(c, new_a, new_b, justification(new normalize_justification(c)));
     }
 
     /**
        \brief Assign \c v to \c m with justification \c tr in the current state.
     */
-    void assign(expr const & m, expr const & v, context const & ctx, trace const & tr) {
+    void assign(expr const & m, expr const & v, context const & ctx, justification const & tr) {
         lean_assert(is_metavar(m));
         metavar_env & menv = m_state.m_menv;
         m_state.m_menv.assign(m, v, tr);
@@ -362,8 +362,8 @@ class elaborator::imp {
             expr tv = m_type_inferer(v, ctx, &menv, ucs);
             for (auto c : ucs)
                 push_front(c);
-            trace new_trace(new typeof_mvar_trace(ctx, m, menv.get_type(m), tv, tr));
-            push_front(mk_convertible_constraint(ctx, tv, menv.get_type(m), new_trace));
+            justification new_jst(new typeof_mvar_justification(ctx, m, menv.get_type(m), tv, tr));
+            push_front(mk_convertible_constraint(ctx, tv, menv.get_type(m), new_jst));
         }
     }
 
@@ -400,16 +400,16 @@ class elaborator::imp {
         if (is_metavar(a)) {
             if (is_assigned(a)) {
                 // Case 1
-                trace new_tr(new substitution_trace(c, get_mvar_trace(a)));
-                push_updated_constraint(c, is_lhs, get_mvar_subst(a), new_tr);
+                justification new_jst(new substitution_justification(c, get_mvar_justification(a)));
+                push_updated_constraint(c, is_lhs, get_mvar_subst(a), new_jst);
                 return Processed;
             } else if (!has_local_context(a)) {
                 // Case 2
                 if (has_metavar(b, a)) {
-                    m_conflict = trace(new unification_failure_trace(c));
+                    m_conflict = justification(new unification_failure_justification(c));
                     return Failed;
                 } else if (allow_assignment) {
-                    assign(a, b, get_context(c), trace(new assignment_trace(c)));
+                    assign(a, b, get_context(c), justification(new assignment_justification(c)));
                     reset_quota();
                     return Processed;
                 }
@@ -418,18 +418,18 @@ class elaborator::imp {
                 if (me.is_lift()) {
                     if (!has_free_var(b, me.s(), me.s() + me.n())) {
                         // Case 3
-                        trace new_tr(new normalize_trace(c));
+                        justification new_jst(new normalize_justification(c));
                         expr new_a = pop_meta_context(a);
                         expr new_b = lower_free_vars(b, me.s() + me.n(), me.n());
                         context new_ctx = get_context(c).remove(me.s(), me.n());
                         if (!is_lhs)
                             swap(new_a, new_b);
-                        push_new_constraint(is_eq(c), new_ctx, new_a, new_b, new_tr);
+                        push_new_constraint(is_eq(c), new_ctx, new_a, new_b, new_jst);
                         return Processed;
                     } else if (is_var(b)) {
                         // Failure, there is no way to unify
                         // ?m[lift:s:n, ...] with a variable in [s, s+n]
-                        m_conflict = trace(new unification_failure_trace(c));
+                        m_conflict = justification(new unification_failure_justification(c));
                         return Failed;
                     }
                 }
@@ -438,34 +438,34 @@ class elaborator::imp {
 
         if (is_app(a) && is_metavar(arg(a, 0)) && is_assigned(arg(a, 0))) {
             // Case 4
-            trace new_tr(new substitution_trace(c, get_mvar_trace(arg(a, 0))));
+            justification new_jst(new substitution_justification(c, get_mvar_justification(arg(a, 0))));
             expr new_a = update_app(a, 0, get_mvar_subst(arg(a, 0)));
-            push_updated_constraint(c, is_lhs, new_a, new_tr);
+            push_updated_constraint(c, is_lhs, new_a, new_jst);
             return Processed;
         }
         return Continue;
     }
 
-    trace mk_subst_trace(unification_constraint const & c, buffer<trace> const & subst_traces) {
-        if (subst_traces.size() == 1) {
-            return trace(new substitution_trace(c, subst_traces[0]));
+    justification mk_subst_justification(unification_constraint const & c, buffer<justification> const & subst_justifications) {
+        if (subst_justifications.size() == 1) {
+            return justification(new substitution_justification(c, subst_justifications[0]));
         } else {
-            return trace(new multi_substitution_trace(c, subst_traces.size(), subst_traces.data()));
+            return justification(new multi_substitution_justification(c, subst_justifications.size(), subst_justifications.data()));
         }
     }
 
     /**
-       \brief Instantiate the assigned metavariables in \c a, and store the justification
-       in \c traces.
+       \brief Instantiate the assigned metavariables in \c a, and store the justifications
+       in \c jsts.
     */
-    expr instantiate_metavars(expr const & a, buffer<trace> & traces) {
+    expr instantiate_metavars(expr const & a, buffer<justification> & jsts) {
         lean_assert(has_assigned_metavar(a));
         metavar_env & menv = m_state.m_menv;
         auto f = [&](expr const & m, unsigned) -> expr {
             if (is_metavar(m) && menv.is_assigned(m)) {
-                trace t = menv.get_trace(m);
+                justification t = menv.get_justification(m);
                 if (t)
-                    traces.push_back(t);
+                    jsts.push_back(t);
                 return menv.get_subst(m);
             } else {
                 return m;
@@ -488,10 +488,10 @@ class elaborator::imp {
         lean_assert(!is_convertible(c) || !is_lhs || is_eqp(convertible_from(c), a));
         lean_assert(!is_convertible(c) ||  is_lhs || is_eqp(convertible_to(c), a));
         if (has_assigned_metavar(a)) {
-            buffer<trace> traces;
-            expr new_a = instantiate_metavars(a, traces);
-            trace new_tr = mk_subst_trace(c, traces);
-            push_updated_constraint(c, is_lhs, new_a, new_tr);
+            buffer<justification> jsts;
+            expr new_a = instantiate_metavars(a, jsts);
+            justification new_jst = mk_subst_justification(c, jsts);
+            push_updated_constraint(c, is_lhs, new_a, new_jst);
             return true;
         } else {
             return false;
@@ -679,11 +679,11 @@ class elaborator::imp {
             buffer<expr> types;
             for (unsigned i = 1; i < num_args(a); i++)
                 types.push_back(lookup(ctx, var_idx(arg(a, i))).get_domain());
-            trace new_trace(new destruct_trace(c));
+            justification new_jst(new destruct_justification(c));
             expr s = mk_lambda(types, b);
             if (!is_lhs)
                 swap(m, s);
-            push_front(mk_eq_constraint(ctx, m, s, new_trace));
+            push_front(mk_eq_constraint(ctx, m, s, new_jst));
             return true;
         } else {
             return false;
@@ -711,7 +711,7 @@ class elaborator::imp {
         for (unsigned i = 1; i < num_a; i++) {
             // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
             state new_state(m_state);
-            trace new_assumption = mk_assumption();
+            justification new_assumption = mk_assumption();
             expr proj            = mk_lambda(arg_types, mk_var(num_a - i - 1));
             expr new_a           = arg(a, i);
             expr new_b           = b;
@@ -723,7 +723,7 @@ class elaborator::imp {
         }
         // Add imitation
         state new_state(m_state);
-        trace new_assumption = mk_assumption();
+        justification new_assumption = mk_assumption();
         expr imitation;
         if (is_app(b)) {
             // Imitation for applications
@@ -829,7 +829,7 @@ class elaborator::imp {
             {
                 // Case 1
                 state new_state(m_state);
-                trace new_assumption = mk_assumption();
+                justification new_assumption = mk_assumption();
                 // add ?m[...] == #1
                 push_new_eq_constraint(new_state.m_queue, ctx, pop_meta_context(a), mk_var(i), new_assumption);
                 // add t == b (t << b)
@@ -843,7 +843,7 @@ class elaborator::imp {
             {
                 // Case 2
                 state new_state(m_state);
-                trace new_assumption = mk_assumption();
+                justification new_assumption = mk_assumption();
                 expr  imitation;
                 if (is_app(b)) {
                     // Imitation for applications b == f(s_1, ..., s_k)
@@ -911,8 +911,8 @@ class elaborator::imp {
             // See comment at process_metavar_inst
             expr imitation = update_abstraction(b, h_1, h_2);
             expr ma  = mk_metavar(metavar_name(a));
-            trace new_tr(new imitation_trace(c));
-            push_new_constraint(true, ctx, ma, imitation, new_tr);
+            justification new_jst(new imitation_justification(c));
+            push_new_constraint(true, ctx, ma, imitation, new_jst);
             return true;
         } else {
             return false;
@@ -934,14 +934,14 @@ class elaborator::imp {
         if (is_lower(c)) {
             // Remark: in principle, there are infinite number of choices.
             // We approximate and only consider the most useful ones.
-            trace new_tr(new destruct_trace(c));
+            justification new_jst(new destruct_justification(c));
             unification_constraint new_c;
             if (a == Bool) {
                 expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
-                new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_tr);
+                new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst);
             } else {
                 expr choices[5] = { a, Type(ty_level(a) + 1), Type(ty_level(a) + 2), TypeM, TypeU };
-                new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_tr);
+                new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst);
             }
             push_front(new_c);
             return true;
@@ -997,17 +997,17 @@ class elaborator::imp {
             // and just check if the upper bound is satisfied.
             //
             // Remark: we also give preference to lower bounds
-            trace new_tr(new destruct_trace(c));
+            justification new_jst(new destruct_justification(c));
             unification_constraint new_c;
             if (b == Type()) {
                 expr choices[2] = { Type(), Bool };
-                new_c = mk_choice_constraint(get_context(c), a, 2, choices, new_tr);
+                new_c = mk_choice_constraint(get_context(c), a, 2, choices, new_jst);
             } else if (b == TypeU) {
                 expr choices[5] = { TypeU, TypeM, Type(level() + 1), Type(), Bool };
-                new_c = mk_choice_constraint(get_context(c), a, 5, choices, new_tr);
+                new_c = mk_choice_constraint(get_context(c), a, 5, choices, new_jst);
             } else if (b == TypeM) {
                 expr choices[4] = { TypeM, Type(level() + 1), Type(), Bool };
-                new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_tr);
+                new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_jst);
             } else {
                 level const & lvl = ty_level(b);
                 lean_assert(!lvl.is_bottom());
@@ -1026,10 +1026,10 @@ class elaborator::imp {
                     if (!L.is_bottom())
                         choices.push_back(Type());
                     choices.push_back(Bool);
-                    new_c = mk_choice_constraint(get_context(c), a, choices.size(), choices.data(), new_tr);
+                    new_c = mk_choice_constraint(get_context(c), a, choices.size(), choices.data(), new_jst);
                 } else if (is_uvar(lvl)) {
                     expr choices[4] = { Type(level() + 1), Type(), b, Bool };
-                    new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_tr);
+                    new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_jst);
                 } else {
                     lean_assert(is_max(lvl));
                     // TODO(Leo)
@@ -1076,45 +1076,45 @@ class elaborator::imp {
                 if (a == b) {
                     return true;
                 } else {
-                    m_conflict = trace(new unification_failure_trace(c));
+                    m_conflict = justification(new unification_failure_justification(c));
                     return false;
                 }
             case expr_kind::Type:
                 if ((!eq && m_env.is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) {
                     return true;
                 } else {
-                    m_conflict = trace(new unification_failure_trace(c));
+                    m_conflict = justification(new unification_failure_justification(c));
                     return false;
                 }
             case expr_kind::Eq: {
-                trace new_trace(new destruct_trace(c));
-                push_front(mk_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_trace));
-                push_front(mk_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_trace));
+                justification new_jst(new destruct_justification(c));
+                push_front(mk_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_jst));
+                push_front(mk_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_jst));
                 return true;
             }
             case expr_kind::Pi: {
-                trace new_trace(new destruct_trace(c));
-                push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_trace));
+                justification new_jst(new destruct_justification(c));
+                push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst));
                 context new_ctx = extend(ctx, abst_name(a), abst_domain(a));
                 if (eq)
-                    push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_trace));
+                    push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst));
                 else
-                    push_front(mk_convertible_constraint(new_ctx, abst_body(a), abst_body(b), new_trace));
+                    push_front(mk_convertible_constraint(new_ctx, abst_body(a), abst_body(b), new_jst));
                 return true;
             }
             case expr_kind::Lambda: {
-                trace new_trace(new destruct_trace(c));
-                push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_trace));
+                justification new_jst(new destruct_justification(c));
+                push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst));
                 context new_ctx = extend(ctx, abst_name(a), abst_domain(a));
-                push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_trace));
+                push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst));
                 return true;
             }
             case expr_kind::App:
                 if (!is_meta_app(a) && !is_meta_app(b)) {
                     if (num_args(a) == num_args(b)) {
-                        trace new_trace(new destruct_trace(c));
+                        justification new_jst(new destruct_justification(c));
                         for (unsigned i = 0; i < num_args(a); i++)
-                            push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_trace));
+                            push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst));
                         return true;
                     } else {
                         return false;
@@ -1135,7 +1135,7 @@ class elaborator::imp {
         }
 
         if (a.kind() != b.kind() && !has_metavar(a) && !has_metavar(b)) {
-            m_conflict = trace(new unification_failure_trace(c));
+            m_conflict = justification(new unification_failure_justification(c));
             return false;
         }
 
@@ -1170,26 +1170,26 @@ class elaborator::imp {
         expr const & lhs1 = max_lhs1(c);
         expr const & lhs2 = max_lhs2(c);
         expr const & rhs  = max_rhs(c);
-        buffer<trace> traces;
+        buffer<justification> jsts;
         bool modified = false;
         expr new_lhs1 = lhs1;
         expr new_lhs2 = lhs2;
         expr new_rhs  = rhs;
         if (has_assigned_metavar(lhs1)) {
-            new_lhs1 = instantiate_metavars(lhs1, traces);
+            new_lhs1 = instantiate_metavars(lhs1, jsts);
             modified = true;
         }
         if (has_assigned_metavar(lhs2)) {
-            new_lhs2 = instantiate_metavars(lhs2, traces);
+            new_lhs2 = instantiate_metavars(lhs2, jsts);
             modified = true;
         }
         if (has_assigned_metavar(rhs)) {
-            new_rhs = instantiate_metavars(rhs, traces);
+            new_rhs = instantiate_metavars(rhs, jsts);
             modified = true;
         }
         if (modified) {
-            trace new_tr = mk_subst_trace(c, traces);
-            push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_tr));
+            justification new_jst = mk_subst_justification(c, jsts);
+            push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst));
             return true;
         }
         if (!is_metavar(lhs1) && !is_type(lhs1)) {
@@ -1205,35 +1205,35 @@ class elaborator::imp {
             modified = (rhs != new_rhs);
         }
         if (modified) {
-            trace new_tr(new normalize_trace(c));
-            push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_tr));
+            justification new_jst(new normalize_justification(c));
+            push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst));
             return true;
         }
         if (is_type(lhs1) && is_type(lhs2)) {
-            trace new_tr(new normalize_trace(c));
+            justification new_jst(new normalize_justification(c));
             expr new_lhs = mk_type(max(ty_level(lhs1), ty_level(lhs2)));
-            push_front(mk_eq_constraint(get_context(c), new_lhs, rhs, new_tr));
+            push_front(mk_eq_constraint(get_context(c), new_lhs, rhs, new_jst));
             return true;
         }
         if (lhs1 == rhs) {
             // ctx |- max(lhs1, lhs2) == rhs
             // ==>  IF lhs1 = rhs
             // ctx |- lhs2 << rhs
-            trace new_tr(new normalize_trace(c));
-            push_front(mk_convertible_constraint(get_context(c), lhs2, rhs, new_tr));
+            justification new_jst(new normalize_justification(c));
+            push_front(mk_convertible_constraint(get_context(c), lhs2, rhs, new_jst));
             return true;
         } else if (lhs2 == rhs) {
             // ctx |- max(lhs1, lhs2) == rhs
             // ==>  IF lhs1 = rhs
             // ctx |- lhs2 << rhs
-            trace new_tr(new normalize_trace(c));
-            push_front(mk_convertible_constraint(get_context(c), lhs1, rhs, new_tr));
+            justification new_jst(new normalize_justification(c));
+            push_front(mk_convertible_constraint(get_context(c), lhs1, rhs, new_jst));
             return true;
         }
 
         if ((!has_metavar(lhs1) && !is_type(lhs1)) ||
             (!has_metavar(lhs2) && !is_type(lhs2))) {
-            m_conflict = trace(new unification_failure_trace(c));
+            m_conflict = justification(new unification_failure_justification(c));
             return false;
         }
 
@@ -1261,9 +1261,9 @@ class elaborator::imp {
             std::unique_ptr<case_split> & d = m_case_splits.back();
             // std::cout << "Assumption " << d->m_curr_assumption.pp(fmt, options(), nullptr, true) << "\n";
             if (depends_on(m_conflict, d->m_curr_assumption)) {
-                d->m_failed_traces.push_back(m_conflict);
+                d->m_failed_justifications.push_back(m_conflict);
                 if (d->next(*this)) {
-                    m_conflict = trace();
+                    m_conflict = justification();
                     reset_quota();
                     return;
                 }
@@ -1283,7 +1283,7 @@ class elaborator::imp {
             push_front(mk_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption));
             return true;
         } else {
-            m_conflict = trace(new unification_failure_by_cases_trace(choice, s.m_failed_traces.size(), s.m_failed_traces.data()));
+            m_conflict = justification(new unification_failure_by_cases_justification(choice, s.m_failed_justifications.size(), s.m_failed_justifications.data()));
             return false;
         }
     }
@@ -1297,7 +1297,7 @@ class elaborator::imp {
             m_state             = s.m_states[sz - idx - 1];
             return true;
         } else {
-            m_conflict = trace(new unification_failure_by_cases_trace(s.m_constraint, s.m_failed_traces.size(), s.m_failed_traces.data()));
+            m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), s.m_failed_justifications.data()));
             return false;
         }
     }
@@ -1313,7 +1313,7 @@ class elaborator::imp {
             }
             return true;
         } catch (exception & ex) {
-            m_conflict = trace(new unification_failure_by_cases_trace(s.m_constraint, s.m_failed_traces.size(), s.m_failed_traces.data()));
+            m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), s.m_failed_justifications.data()));
             return false;
         }
     }
@@ -1340,16 +1340,16 @@ public:
         if (m_conflict)
             throw elaborator_exception(m_conflict);
         if (!m_case_splits.empty()) {
-            buffer<trace> assumptions;
+            buffer<justification> assumptions;
             for (std::unique_ptr<case_split> const & cs : m_case_splits)
                 assumptions.push_back(cs->m_curr_assumption);
-            m_conflict = trace(new next_solution_trace(assumptions.size(), assumptions.data()));
+            m_conflict = justification(new next_solution_justification(assumptions.size(), assumptions.data()));
             resolve_conflict();
         } else if (m_first) {
             m_first = false;
         } else {
             // this is not the first run, and there are no case-splits
-            m_conflict = trace(new next_solution_trace(0, nullptr));
+            m_conflict = justification(new next_solution_justification(0, nullptr));
             throw elaborator_exception(m_conflict);
         }
         reset_quota();
@@ -1410,7 +1410,7 @@ elaborator::elaborator(environment const & env,
 elaborator::elaborator(environment const & env,
                        metavar_env const & menv,
                        context const & ctx, expr const & lhs, expr const & rhs):
-    elaborator(env, menv, { mk_eq_constraint(ctx, lhs, rhs, trace()) }) {
+    elaborator(env, menv, { mk_eq_constraint(ctx, lhs, rhs, justification()) }) {
 }
 
 elaborator::~elaborator() {
diff --git a/src/library/elaborator/elaborator_exception.h b/src/library/elaborator/elaborator_exception.h
index 3c07bbf8e..7c4bce966 100644
--- a/src/library/elaborator/elaborator_exception.h
+++ b/src/library/elaborator/elaborator_exception.h
@@ -6,20 +6,20 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "util/exception.h"
-#include "kernel/trace.h"
+#include "kernel/justification.h"
 
 namespace lean {
 /**
    \brief Elaborator and related components store the reason for
-   failure in trace objects.
+   failure in justification objects.
 */
 class elaborator_exception : public exception {
-    trace m_trace;
+    justification m_justification;
 public:
-    elaborator_exception(trace const & tr):m_trace(tr) {}
+    elaborator_exception(justification const & j):m_justification(j) {}
     virtual ~elaborator_exception() {}
     virtual char const * what() const noexcept { return "elaborator exception"; }
-    trace const & get_trace() const { return m_trace; }
+    justification const & get_justification() const { return m_justification; }
 };
 
 
diff --git a/src/library/elaborator/elaborator_justification.cpp b/src/library/elaborator/elaborator_justification.cpp
new file mode 100644
index 000000000..368d5f7b5
--- /dev/null
+++ b/src/library/elaborator/elaborator_justification.cpp
@@ -0,0 +1,187 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/elaborator/elaborator_justification.h"
+
+namespace lean {
+static void push_back(buffer<justification_cell*> & r, justification const & t) {
+    if (t)
+        r.push_back(t.raw());
+}
+
+template<typename T>
+static void append(buffer<justification_cell*> & r, T const & s) {
+    for (auto t : s)
+        push_back(r, t);
+}
+
+// -------------------------
+// Assumptions
+// -------------------------
+assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {
+}
+void assumption_justification::get_children(buffer<justification_cell*> &) const {
+}
+expr const & assumption_justification::get_main_expr() const {
+    return expr::null();
+}
+format assumption_justification::pp_header(formatter const &, options const &) const {
+    return format{format("assumption"), space(), format(m_idx)};
+}
+
+// -------------------------
+// Propagation justification
+// -------------------------
+propagation_justification::propagation_justification(unification_constraint const & c):
+    m_constraint(c) {
+}
+propagation_justification::~propagation_justification() {
+}
+void propagation_justification::get_children(buffer<justification_cell*> & r) const {
+    push_back(r, m_constraint.get_justification());
+}
+expr const & propagation_justification::get_main_expr() const {
+    return expr::null();
+}
+format propagation_justification::pp_header(formatter const & fmt, options const & opts) const {
+    format r;
+    r += format(get_prop_name());
+    r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false));
+    return r;
+}
+
+// -------------------------
+// Unification failure (by cases)
+// -------------------------
+unification_failure_by_cases_justification::unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs):
+    unification_failure_justification(c),
+    m_cases(cs, cs + num) {
+}
+unification_failure_by_cases_justification::~unification_failure_by_cases_justification() {
+}
+void unification_failure_by_cases_justification::get_children(buffer<justification_cell*> & r) const {
+    push_back(r, get_constraint().get_justification());
+    append(r, m_cases);
+}
+
+// -------------------------
+// Substitution justification
+// -------------------------
+substitution_justification::substitution_justification(unification_constraint const & c, justification const & t):
+    propagation_justification(c),
+    m_assignment_justification(t) {
+}
+substitution_justification::~substitution_justification() {
+}
+void substitution_justification::get_children(buffer<justification_cell*> & r) const {
+    propagation_justification::get_children(r);
+    push_back(r, m_assignment_justification);
+}
+
+multi_substitution_justification::multi_substitution_justification(unification_constraint const & c, unsigned num, justification const * ts):
+    propagation_justification(c),
+    m_assignment_justifications(ts, ts + num) {
+}
+multi_substitution_justification::~multi_substitution_justification() {
+}
+void multi_substitution_justification::get_children(buffer<justification_cell*> & r) const {
+    propagation_justification::get_children(r);
+    append(r, m_assignment_justifications);
+}
+
+// -------------------------
+// typeof metavar justification
+// -------------------------
+typeof_mvar_justification::typeof_mvar_justification(context const & ctx, expr const & m, expr const & tm, expr const & t, justification const & tr):
+    m_context(ctx),
+    m_mvar(m),
+    m_typeof_mvar(tm),
+    m_type(t),
+    m_justification(tr) {
+}
+typeof_mvar_justification::~typeof_mvar_justification() {
+}
+format typeof_mvar_justification::pp_header(formatter const & fmt, options const & opts) const {
+    format r;
+    unsigned indent = get_pp_indent(opts);
+    r += format("Propagate type,");
+    {
+        format body;
+        body += fmt(m_context, m_mvar, false, opts);
+        body += space();
+        body += colon();
+        body += nest(indent, compose(line(), fmt(m_context, m_typeof_mvar, false, opts)));
+        r += nest(indent, compose(line(), body));
+    }
+    return group(r);
+}
+void typeof_mvar_justification::get_children(buffer<justification_cell*> & r) const {
+    push_back(r, m_justification);
+}
+
+// -------------------------
+// Synthesis justification objects
+// -------------------------
+synthesis_justification::synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs):
+    m_context(ctx),
+    m_mvar(mvar),
+    m_type(type),
+    m_substitution_justifications(substs, substs + num) {
+}
+synthesis_justification::~synthesis_justification() {
+}
+format synthesis_justification::pp_header(formatter const & fmt, options const & opts) const {
+    format r;
+    r += format(get_label());
+    r += space();
+    r += fmt(m_context, m_mvar, false, opts);
+    unsigned indent = get_pp_indent(opts);
+    r += nest(indent, compose(line(), fmt(m_context, m_type, true, opts)));
+    return r;
+}
+void synthesis_justification::get_children(buffer<justification_cell*> & r) const {
+    append(r, m_substitution_justifications);
+}
+expr const & synthesis_justification::get_main_expr() const {
+    return m_mvar;
+}
+
+char const * synthesis_failure_justification::get_label() const {
+    return "Failed to synthesize expression of type for";
+}
+synthesis_failure_justification::synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs):
+    synthesis_justification(ctx, mvar, type, num, substs),
+    m_justification(tr) {
+}
+synthesis_failure_justification::~synthesis_failure_justification() {
+}
+void synthesis_failure_justification::get_children(buffer<justification_cell*> & r) const {
+    synthesis_justification::get_children(r);
+    push_back(r, m_justification);
+}
+
+char const * synthesized_assignment_justification::get_label() const {
+    return "Synthesized assignment for";
+}
+
+// -------------------------
+// Next solution justification
+// -------------------------
+next_solution_justification::next_solution_justification(unsigned num, justification const * as):
+    m_assumptions(as, as + num) {
+}
+next_solution_justification::~next_solution_justification() {
+}
+format next_solution_justification::pp_header(formatter const &, options const &) const {
+    return format("next solution");
+}
+void next_solution_justification::get_children(buffer<justification_cell*> & r) const {
+    append(r, m_assumptions);
+}
+expr const & next_solution_justification::get_main_expr() const {
+    return expr::null();
+}
+}
diff --git a/src/library/elaborator/elaborator_justification.h b/src/library/elaborator/elaborator_justification.h
new file mode 100644
index 000000000..87c4586a5
--- /dev/null
+++ b/src/library/elaborator/elaborator_justification.h
@@ -0,0 +1,229 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <vector>
+#include "kernel/justification.h"
+#include "kernel/unification_constraint.h"
+
+namespace lean {
+/**
+   \brief Base class for justification objects used to justify case-splits.
+*/
+class assumption_justification : public justification_cell {
+    unsigned m_idx;
+public:
+    assumption_justification(unsigned idx);
+    virtual void get_children(buffer<justification_cell*> &) const;
+    virtual expr const & get_main_expr() const;
+    virtual format pp_header(formatter const &, options const &) const;
+};
+
+/**
+   \brief Base class for justifying propagations and failures
+*/
+class propagation_justification : public justification_cell {
+    unification_constraint m_constraint;
+protected:
+    /** \brief Auxiliary method used by pp_header to label a propagation step, subclasses must redefine it. */
+    virtual char const * get_prop_name() const = 0;
+public:
+    propagation_justification(unification_constraint const & c);
+    virtual ~propagation_justification();
+    virtual void get_children(buffer<justification_cell*> & r) const;
+    virtual expr const & get_main_expr() const;
+    virtual format pp_header(formatter const &, options const &) const;
+    unification_constraint const & get_constraint() const { return m_constraint; }
+};
+
+/**
+   \brief Justification object used to mark that a particular unification constraint could not be solved.
+*/
+class unification_failure_justification : public propagation_justification {
+protected:
+    virtual char const * get_prop_name() const { return "Failed to solve"; }
+public:
+    unification_failure_justification(unification_constraint const & c):propagation_justification(c) {}
+};
+
+/**
+   \brief Justification object created for justifying that a constraint that
+   generated a case-split does not have a solution. Each case-split
+   corresponds to a different way of solving the constraint.
+*/
+class unification_failure_by_cases_justification : public unification_failure_justification {
+    std::vector<justification> m_cases; // why each case failed
+public:
+    unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs);
+    virtual ~unification_failure_by_cases_justification();
+    virtual void get_children(buffer<justification_cell*> & r) const;
+};
+
+/**
+   \brief Justification object used to justify a metavar assignment.
+*/
+class assignment_justification : public propagation_justification {
+protected:
+    virtual char const * get_prop_name() const { return "Assignment"; }
+public:
+    assignment_justification(unification_constraint const & c):propagation_justification(c) {}
+};
+
+/**
+   \brief Justification object used to justify simple structural steps when processing unification
+   constraints. For example, given the constraint
+
+   <tt>ctx |- (f a) == (f b)</tt>
+
+   where \c f is a variable, we must have
+
+   <tt>ctx |- a == b</tt>
+
+   The justification for the latter is a destruct justification based on the former.
+*/
+class destruct_justification : public propagation_justification {
+protected:
+    virtual char const * get_prop_name() const { return "Destruct/Decompose"; }
+public:
+    destruct_justification(unification_constraint const & c):propagation_justification(c) {}
+};
+
+/**
+   \brief Justification object used to justify a normalization step such as.
+
+   <tt>ctx |- (fun x : T, x) a == b</tt>
+   ==>
+   <tt>ctx |- a == b</tt>
+*/
+class normalize_justification : public propagation_justification {
+protected:
+    virtual char const * get_prop_name() const { return "Normalize"; }
+public:
+    normalize_justification(unification_constraint const & c):propagation_justification(c) {}
+};
+
+/**
+   \brief Justification object used to justify an imitation step.
+   An imitation step is used when solving constraints such as:
+
+   <tt>ctx |- ?m[lift:s:n, ...] == Pi (x : A), B x</tt>
+
+   In this case, ?m must be a Pi. We make progress, by adding the constraint
+   <tt>ctx |- ?m == Pi (x : ?M1), (?M2 x)</tt>
+
+   where ?M1 and ?M2 are fresh metavariables.
+*/
+class imitation_justification : public propagation_justification {
+protected:
+    virtual char const * get_prop_name() const { return "Imitation"; }
+public:
+    imitation_justification(unification_constraint const & c):propagation_justification(c) {}
+};
+
+/**
+   \brief Justification object used to justify a new constraint obtained by substitution.
+*/
+class substitution_justification : public propagation_justification {
+    justification                  m_assignment_justification;
+protected:
+    virtual char const * get_prop_name() const { return "Substitution"; }
+public:
+    substitution_justification(unification_constraint const & c, justification const & t);
+    virtual ~substitution_justification();
+    virtual void get_children(buffer<justification_cell*> & r) const;
+};
+
+/**
+   \brief Justification object used to justify a new constraint obtained by multiple substitution.
+*/
+class multi_substitution_justification : public propagation_justification {
+    std::vector<justification>    m_assignment_justifications;
+protected:
+    virtual char const * get_prop_name() const { return "Substitution"; }
+public:
+    multi_substitution_justification(unification_constraint const & c, unsigned num, justification const * ts);
+    virtual ~multi_substitution_justification();
+    virtual void get_children(buffer<justification_cell*> & r) const;
+};
+
+/**
+   \brief Justification object used to justify a <tt>typeof(m) == t</tt> constraint generated when
+   we assign a metavariable \c m.
+*/
+class typeof_mvar_justification : public justification_cell {
+    context m_context;
+    expr    m_mvar;
+    expr    m_typeof_mvar;
+    expr    m_type;
+    justification   m_justification;
+public:
+    typeof_mvar_justification(context const & ctx, expr const & m, expr const & mt, expr const & t, justification const & tr);
+    virtual ~typeof_mvar_justification();
+    virtual format pp_header(formatter const &, options const &) const;
+    virtual void get_children(buffer<justification_cell*> & r) const;
+};
+
+/**
+   \brief Base class for synthesis_failure_justification and synthesized_assignment_justification
+*/
+class synthesis_justification : public justification_cell {
+    context            m_context;
+    expr               m_mvar;
+    expr               m_type;
+    std::vector<justification> m_substitution_justifications; // justification objects justifying the assignments used to instantiate \c m_type and \c m_context.
+protected:
+    virtual char const * get_label() const = 0;
+public:
+    synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs);
+    virtual ~synthesis_justification();
+    virtual format pp_header(formatter const &, options const &) const;
+    virtual void get_children(buffer<justification_cell*> & r) const;
+    virtual expr const & get_main_expr() const;
+};
+
+/**
+   \brief Justification object for justifying why a synthesis step failed.
+   A synthesis step is of the form
+
+   <tt>ctx |- ?mvar : type</tt>
+
+   Before invoking the synthesizer, the elaborator substitutes the
+   metavariables in \c ctx and \c type with their corresponding assignments.
+*/
+class synthesis_failure_justification : public synthesis_justification {
+    justification              m_justification;  // justification object produced by the synthesizer
+protected:
+    virtual char const * get_label() const;
+public:
+    synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs);
+    virtual ~synthesis_failure_justification();
+    virtual void get_children(buffer<justification_cell*> & r) const;
+};
+
+/**
+   \brief Justification object used to justify a metavar assignment produced by a synthesizer.
+*/
+class synthesized_assignment_justification : public synthesis_justification {
+protected:
+    virtual char const * get_label() const;
+public:
+    synthesized_assignment_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs):
+        synthesis_justification(ctx, mvar, type, num, substs) {
+    }
+};
+
+/**
+    \brief Justification object used to justify that we are moving to the next solution.
+*/
+class next_solution_justification : public justification_cell {
+    std::vector<justification> m_assumptions; // Set of assumptions used to derive last solution
+public:
+    next_solution_justification(unsigned num, justification const * as);
+    virtual ~next_solution_justification();
+    virtual format pp_header(formatter const &, options const &) const;
+    virtual void get_children(buffer<justification_cell*> & r) const;
+    virtual expr const & get_main_expr() const;
+};
+};
diff --git a/src/library/elaborator/elaborator_plugin.h b/src/library/elaborator/elaborator_plugin.h
index e8d7316ff..60273b305 100644
--- a/src/library/elaborator/elaborator_plugin.h
+++ b/src/library/elaborator/elaborator_plugin.h
@@ -27,7 +27,7 @@ public:
             Each result is represented by a pair: the new metavariable
             environment and a new list of constraints to be solved.
         */
-        virtual std::pair<metavar_env, list<unification_constraint>> next(trace const & assumption) = 0;
+        virtual std::pair<metavar_env, list<unification_constraint>> next(justification const & assumption) = 0;
         /** \brief Interrupt the computation for the next solution. */
         virtual void interrupt() = 0;
     };
diff --git a/src/library/elaborator/elaborator_trace.cpp b/src/library/elaborator/elaborator_trace.cpp
deleted file mode 100644
index 6fa753c8a..000000000
--- a/src/library/elaborator/elaborator_trace.cpp
+++ /dev/null
@@ -1,187 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/elaborator/elaborator_trace.h"
-
-namespace lean {
-static void push_back(buffer<trace_cell*> & r, trace const & t) {
-    if (t)
-        r.push_back(t.raw());
-}
-
-template<typename T>
-static void append(buffer<trace_cell*> & r, T const & s) {
-    for (auto t : s)
-        push_back(r, t);
-}
-
-// -------------------------
-// Assumptions
-// -------------------------
-assumption_trace::assumption_trace(unsigned idx):m_idx(idx) {
-}
-void assumption_trace::get_children(buffer<trace_cell*> &) const {
-}
-expr const & assumption_trace::get_main_expr() const {
-    return expr::null();
-}
-format assumption_trace::pp_header(formatter const &, options const &) const {
-    return format{format("assumption"), space(), format(m_idx)};
-}
-
-// -------------------------
-// Propagation trace
-// -------------------------
-propagation_trace::propagation_trace(unification_constraint const & c):
-    m_constraint(c) {
-}
-propagation_trace::~propagation_trace() {
-}
-void propagation_trace::get_children(buffer<trace_cell*> & r) const {
-    push_back(r, m_constraint.get_trace());
-}
-expr const & propagation_trace::get_main_expr() const {
-    return expr::null();
-}
-format propagation_trace::pp_header(formatter const & fmt, options const & opts) const {
-    format r;
-    r += format(get_prop_name());
-    r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false));
-    return r;
-}
-
-// -------------------------
-// Unification failure (by cases)
-// -------------------------
-unification_failure_by_cases_trace::unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs):
-    unification_failure_trace(c),
-    m_cases(cs, cs + num) {
-}
-unification_failure_by_cases_trace::~unification_failure_by_cases_trace() {
-}
-void unification_failure_by_cases_trace::get_children(buffer<trace_cell*> & r) const {
-    push_back(r, get_constraint().get_trace());
-    append(r, m_cases);
-}
-
-// -------------------------
-// Substitution trace
-// -------------------------
-substitution_trace::substitution_trace(unification_constraint const & c, trace const & t):
-    propagation_trace(c),
-    m_assignment_trace(t) {
-}
-substitution_trace::~substitution_trace() {
-}
-void substitution_trace::get_children(buffer<trace_cell*> & r) const {
-    propagation_trace::get_children(r);
-    push_back(r, m_assignment_trace);
-}
-
-multi_substitution_trace::multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts):
-    propagation_trace(c),
-    m_assignment_traces(ts, ts + num) {
-}
-multi_substitution_trace::~multi_substitution_trace() {
-}
-void multi_substitution_trace::get_children(buffer<trace_cell*> & r) const {
-    propagation_trace::get_children(r);
-    append(r, m_assignment_traces);
-}
-
-// -------------------------
-// typeof metavar trace
-// -------------------------
-typeof_mvar_trace::typeof_mvar_trace(context const & ctx, expr const & m, expr const & tm, expr const & t, trace const & tr):
-    m_context(ctx),
-    m_mvar(m),
-    m_typeof_mvar(tm),
-    m_type(t),
-    m_trace(tr) {
-}
-typeof_mvar_trace::~typeof_mvar_trace() {
-}
-format typeof_mvar_trace::pp_header(formatter const & fmt, options const & opts) const {
-    format r;
-    unsigned indent = get_pp_indent(opts);
-    r += format("Propagate type,");
-    {
-        format body;
-        body += fmt(m_context, m_mvar, false, opts);
-        body += space();
-        body += colon();
-        body += nest(indent, compose(line(), fmt(m_context, m_typeof_mvar, false, opts)));
-        r += nest(indent, compose(line(), body));
-    }
-    return group(r);
-}
-void typeof_mvar_trace::get_children(buffer<trace_cell*> & r) const {
-    push_back(r, m_trace);
-}
-
-// -------------------------
-// Synthesis trace objects
-// -------------------------
-synthesis_trace::synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs):
-    m_context(ctx),
-    m_mvar(mvar),
-    m_type(type),
-    m_substitution_traces(substs, substs + num) {
-}
-synthesis_trace::~synthesis_trace() {
-}
-format synthesis_trace::pp_header(formatter const & fmt, options const & opts) const {
-    format r;
-    r += format(get_label());
-    r += space();
-    r += fmt(m_context, m_mvar, false, opts);
-    unsigned indent = get_pp_indent(opts);
-    r += nest(indent, compose(line(), fmt(m_context, m_type, true, opts)));
-    return r;
-}
-void synthesis_trace::get_children(buffer<trace_cell*> & r) const {
-    append(r, m_substitution_traces);
-}
-expr const & synthesis_trace::get_main_expr() const {
-    return m_mvar;
-}
-
-char const * synthesis_failure_trace::get_label() const {
-    return "Failed to synthesize expression of type for";
-}
-synthesis_failure_trace::synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs):
-    synthesis_trace(ctx, mvar, type, num, substs),
-    m_trace(tr) {
-}
-synthesis_failure_trace::~synthesis_failure_trace() {
-}
-void synthesis_failure_trace::get_children(buffer<trace_cell*> & r) const {
-    synthesis_trace::get_children(r);
-    push_back(r, m_trace);
-}
-
-char const * synthesized_assignment_trace::get_label() const {
-    return "Synthesized assignment for";
-}
-
-// -------------------------
-// Next solution trace
-// -------------------------
-next_solution_trace::next_solution_trace(unsigned num, trace const * as):
-    m_assumptions(as, as + num) {
-}
-next_solution_trace::~next_solution_trace() {
-}
-format next_solution_trace::pp_header(formatter const &, options const &) const {
-    return format("next solution");
-}
-void next_solution_trace::get_children(buffer<trace_cell*> & r) const {
-    append(r, m_assumptions);
-}
-expr const & next_solution_trace::get_main_expr() const {
-    return expr::null();
-}
-}
diff --git a/src/library/elaborator/elaborator_trace.h b/src/library/elaborator/elaborator_trace.h
deleted file mode 100644
index e5d7266f6..000000000
--- a/src/library/elaborator/elaborator_trace.h
+++ /dev/null
@@ -1,229 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <vector>
-#include "kernel/trace.h"
-#include "kernel/unification_constraint.h"
-
-namespace lean {
-/**
-   \brief Base class for trace objects used to justify case-splits.
-*/
-class assumption_trace : public trace_cell {
-    unsigned m_idx;
-public:
-    assumption_trace(unsigned idx);
-    virtual void get_children(buffer<trace_cell*> &) const;
-    virtual expr const & get_main_expr() const;
-    virtual format pp_header(formatter const &, options const &) const;
-};
-
-/**
-   \brief Base class for justifying propagations and failures
-*/
-class propagation_trace : public trace_cell {
-    unification_constraint m_constraint;
-protected:
-    /** \brief Auxiliary method used by pp_header to label a propagation step, subclasses must redefine it. */
-    virtual char const * get_prop_name() const = 0;
-public:
-    propagation_trace(unification_constraint const & c);
-    virtual ~propagation_trace();
-    virtual void get_children(buffer<trace_cell*> & r) const;
-    virtual expr const & get_main_expr() const;
-    virtual format pp_header(formatter const &, options const &) const;
-    unification_constraint const & get_constraint() const { return m_constraint; }
-};
-
-/**
-   \brief Trace object used to mark that a particular unification constraint could not be solved.
-*/
-class unification_failure_trace : public propagation_trace {
-protected:
-    virtual char const * get_prop_name() const { return "Failed to solve"; }
-public:
-    unification_failure_trace(unification_constraint const & c):propagation_trace(c) {}
-};
-
-/**
-   \brief Trace object created for justifying that a constraint that
-   generated a case-split does not have a solution. Each case-split
-   corresponds to a different way of solving the constraint.
-*/
-class unification_failure_by_cases_trace : public unification_failure_trace {
-    std::vector<trace> m_cases; // why each case failed
-public:
-    unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs);
-    virtual ~unification_failure_by_cases_trace();
-    virtual void get_children(buffer<trace_cell*> & r) const;
-};
-
-/**
-   \brief Trace object used to justify a metavar assignment.
-*/
-class assignment_trace : public propagation_trace {
-protected:
-    virtual char const * get_prop_name() const { return "Assignment"; }
-public:
-    assignment_trace(unification_constraint const & c):propagation_trace(c) {}
-};
-
-/**
-   \brief Trace object used to justify simple structural steps when processing unification
-   constraints. For example, given the constraint
-
-   <tt>ctx |- (f a) == (f b)</tt>
-
-   where \c f is a variable, we must have
-
-   <tt>ctx |- a == b</tt>
-
-   The justification for the latter is a destruct trace based on the former.
-*/
-class destruct_trace : public propagation_trace {
-protected:
-    virtual char const * get_prop_name() const { return "Destruct/Decompose"; }
-public:
-    destruct_trace(unification_constraint const & c):propagation_trace(c) {}
-};
-
-/**
-   \brief Trace object used to justify a normalization step such as.
-
-   <tt>ctx |- (fun x : T, x) a == b</tt>
-   ==>
-   <tt>ctx |- a == b</tt>
-*/
-class normalize_trace : public propagation_trace {
-protected:
-    virtual char const * get_prop_name() const { return "Normalize"; }
-public:
-    normalize_trace(unification_constraint const & c):propagation_trace(c) {}
-};
-
-/**
-   \brief Trace object used to justify an imitation step.
-   An imitation step is used when solving constraints such as:
-
-   <tt>ctx |- ?m[lift:s:n, ...] == Pi (x : A), B x</tt>
-
-   In this case, ?m must be a Pi. We make progress, by adding the constraint
-   <tt>ctx |- ?m == Pi (x : ?M1), (?M2 x)</tt>
-
-   where ?M1 and ?M2 are fresh metavariables.
-*/
-class imitation_trace : public propagation_trace {
-protected:
-    virtual char const * get_prop_name() const { return "Imitation"; }
-public:
-    imitation_trace(unification_constraint const & c):propagation_trace(c) {}
-};
-
-/**
-   \brief Trace object used to justify a new constraint obtained by substitution.
-*/
-class substitution_trace : public propagation_trace {
-    trace                  m_assignment_trace;
-protected:
-    virtual char const * get_prop_name() const { return "Substitution"; }
-public:
-    substitution_trace(unification_constraint const & c, trace const & t);
-    virtual ~substitution_trace();
-    virtual void get_children(buffer<trace_cell*> & r) const;
-};
-
-/**
-   \brief Trace object used to justify a new constraint obtained by multiple substitution.
-*/
-class multi_substitution_trace : public propagation_trace {
-    std::vector<trace>    m_assignment_traces;
-protected:
-    virtual char const * get_prop_name() const { return "Substitution"; }
-public:
-    multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts);
-    virtual ~multi_substitution_trace();
-    virtual void get_children(buffer<trace_cell*> & r) const;
-};
-
-/**
-   \brief Trace object used to justify a <tt>typeof(m) == t</tt> constraint generated when
-   we assign a metavariable \c m.
-*/
-class typeof_mvar_trace : public trace_cell {
-    context m_context;
-    expr    m_mvar;
-    expr    m_typeof_mvar;
-    expr    m_type;
-    trace   m_trace;
-public:
-    typeof_mvar_trace(context const & ctx, expr const & m, expr const & mt, expr const & t, trace const & tr);
-    virtual ~typeof_mvar_trace();
-    virtual format pp_header(formatter const &, options const &) const;
-    virtual void get_children(buffer<trace_cell*> & r) const;
-};
-
-/**
-   \brief Base class for synthesis_failure_trace and synthesized_assignment_trace
-*/
-class synthesis_trace : public trace_cell {
-    context            m_context;
-    expr               m_mvar;
-    expr               m_type;
-    std::vector<trace> m_substitution_traces; // trace objects justifying the assignments used to instantiate \c m_type and \c m_context.
-protected:
-    virtual char const * get_label() const = 0;
-public:
-    synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs);
-    virtual ~synthesis_trace();
-    virtual format pp_header(formatter const &, options const &) const;
-    virtual void get_children(buffer<trace_cell*> & r) const;
-    virtual expr const & get_main_expr() const;
-};
-
-/**
-   \brief Trace object for justifying why a synthesis step failed.
-   A synthesis step is of the form
-
-   <tt>ctx |- ?mvar : type</tt>
-
-   Before invoking the synthesizer, the elaborator substitutes the
-   metavariables in \c ctx and \c type with their corresponding assignments.
-*/
-class synthesis_failure_trace : public synthesis_trace {
-    trace              m_trace;  // trace object produced by the synthesizer
-protected:
-    virtual char const * get_label() const;
-public:
-    synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs);
-    virtual ~synthesis_failure_trace();
-    virtual void get_children(buffer<trace_cell*> & r) const;
-};
-
-/**
-   \brief Trace object used to justify a metavar assignment produced by a synthesizer.
-*/
-class synthesized_assignment_trace : public synthesis_trace {
-protected:
-    virtual char const * get_label() const;
-public:
-    synthesized_assignment_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs):
-        synthesis_trace(ctx, mvar, type, num, substs) {
-    }
-};
-
-/**
-    \brief Trace object used to justify that we are moving to the next solution.
-*/
-class next_solution_trace : public trace_cell {
-    std::vector<trace> m_assumptions; // Set of assumptions used to derive last solution
-public:
-    next_solution_trace(unsigned num, trace const * as);
-    virtual ~next_solution_trace();
-    virtual format pp_header(formatter const &, options const &) const;
-    virtual void get_children(buffer<trace_cell*> & r) const;
-    virtual expr const & get_main_expr() const;
-};
-};
diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp
index d1bb6ee99..06f474de6 100644
--- a/src/library/type_inferer.cpp
+++ b/src/library/type_inferer.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/builtin.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/type_checker_trace.h"
+#include "kernel/type_checker_justification.h"
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
 #include "kernel/metavar.h"
@@ -47,8 +47,8 @@ class type_inferer::imp {
         if (u == Bool)
             return Type();
         if (has_metavar(u) && m_menv) {
-            trace tr = mk_type_expected_trace(ctx, s);
-            m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, tr));
+            justification jst = mk_type_expected_justification(ctx, s);
+            m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
             return u;
         }
         throw type_expected_exception(m_env, ctx, s);
@@ -70,8 +70,8 @@ class type_inferer::imp {
                     expr A   = m_menv->mk_metavar(ctx);
                     expr B   = m_menv->mk_metavar(ctx);
                     expr p   = mk_pi(g_x_name, A, B(Var(0)));
-                    trace tr = mk_function_expected_trace(ctx, e);
-                    m_uc->push_back(mk_eq_constraint(ctx, t, p, tr));
+                    justification jst = mk_function_expected_justification(ctx, e);
+                    m_uc->push_back(mk_eq_constraint(ctx, t, p, jst));
                     t        = abst_body(p);
                 } else {
                     throw function_expected_exception(m_env, ctx, e);
@@ -186,9 +186,9 @@ class type_inferer::imp {
                 r = mk_type(max(ty_level(t1), ty_level(t2)));
             } else {
                 lean_assert(m_uc);
-                trace tr = mk_max_type_trace(ctx, e);
+                justification jst = mk_max_type_justification(ctx, e);
                 r = m_menv->mk_metavar(ctx);
-                m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, tr));
+                m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, jst));
             }
             break;
         }
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 3cd9c7386..f41c232b8 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/printer.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/type_checker_trace.h"
+#include "kernel/type_checker_justification.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
 #include "library/all/all.h"
@@ -297,7 +297,7 @@ static void tst15() {
     lean_assert(is_eqp(r, checker.infer_type(F, ctx1)));
 }
 
-static void check_trace_msg(trace const & t, char const * expected) {
+static void check_justification_msg(justification const & t, char const * expected) {
     formatter fmt = mk_simple_formatter();
     options   opts;
     opts = opts.update({"pp", "indent"}, 2);
@@ -309,18 +309,18 @@ static void check_trace_msg(trace const & t, char const * expected) {
 }
 
 static void tst16() {
-    std::cout << "Testing type checker trace objects\n";
+    std::cout << "Testing type checker justification objects\n";
     context ctx;
     expr f = Const("f");
     expr a = Const("a");
     expr x = Var(0);
     ctx = extend(ctx, "x", Const("N"));
-    check_trace_msg(mk_function_expected_trace(ctx, f(a, x)), "Function expected at\n  f a x");
-    check_trace_msg(mk_type_expected_trace(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
-    check_trace_msg(mk_type_expected_trace(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n  Pi a : N, (x a)");
-    check_trace_msg(mk_app_type_match_trace(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n  f\nwith arguments:\n  a\n  x");
-    check_trace_msg(mk_max_type_trace(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
-    check_trace_msg(mk_def_type_match_trace(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
+    check_justification_msg(mk_function_expected_justification(ctx, f(a, x)), "Function expected at\n  f a x");
+    check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
+    check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n  Pi a : N, (x a)");
+    check_justification_msg(mk_app_type_match_justification(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n  f\nwith arguments:\n  a\n  x");
+    check_justification_msg(mk_max_type_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
+    check_justification_msg(mk_def_type_match_justification(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
 }
 
 int main() {
diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp
index a53b913ed..0093f4e14 100644
--- a/src/tests/library/elaborator/elaborator.cpp
+++ b/src/tests/library/elaborator/elaborator.cpp
@@ -51,9 +51,9 @@ static void tst1() {
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
     expr int_id = Fun({a, Int}, a);
     expr nat_id = Fun({a, Nat}, a);
-    ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, trace()));
-    ucs.push_back(mk_choice_constraint(context(), m2, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
-    ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, trace()));
+    ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, justification()));
+    ucs.push_back(mk_choice_constraint(context(), m2, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
+    ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
 }
@@ -93,9 +93,9 @@ static void tst2() {
     expr F  = m1(g(m2, m3(a)), m4(nVal(0)));
     std::cout << F << "\n";
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
-    ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
-    ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, trace()));
-    ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
+    ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
+    ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
+    ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
 }
@@ -136,9 +136,9 @@ static void tst3() {
     expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a));
     std::cout << F << "\n";
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
-    ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
-    ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
-    ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, trace()));
+    ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
+    ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
+    ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
 }
@@ -181,8 +181,8 @@ static void tst4() {
     expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b);
     std::cout << F << "\n";
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
-    ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
-    ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, trace()));
+    ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
+    ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
 }
@@ -223,7 +223,7 @@ static void tst5() {
     expr F = Fun({{x, m1}, {y, m2}}, f(m3, x, y))(m4(a), b);
     std::cout << F << "\n";
     std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
-    ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, trace()));
+    ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
 }
@@ -260,7 +260,7 @@ static void tst6() {
     expr V = Subst(m1, m2, m3, m4, H1, H2);
     expr expected = Eq(f(a, f(b, b)), a);
     expr given    = checker.infer_type(V, context(), &menv, ucs);
-    ucs.push_back(mk_eq_constraint(context(), expected, given, trace()));
+    ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
     elaborator elb(env, menv, ucs.size(), ucs.data());
     substitution s = elb.next();
     std::cout << beta_reduce(instantiate_metavars(V, s)) << "\n";