diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index d4abeb230..99dac5603 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -2,10 +2,10 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
 instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
 object.cpp environment.cpp replace_visitor.cpp io_state.cpp
-normalizer.cpp
-# type_checker.cpp kernel.cpp
-# justification.cpp unification_constraint.cpp
-# type_checker_justification.cpp pos_info_provider.cpp
+normalizer.cpp justification.cpp pos_info_provider.cpp
+# type_checker.cpp
+#  unification_constraint.cpp
+# type_checker_justification.cpp
 )
 
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp
index 236a13d75..7919827d4 100644
--- a/src/kernel/justification.cpp
+++ b/src/kernel/justification.cpp
@@ -6,76 +6,232 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include "util/buffer.h"
+#include "util/int64.h"
 #include "kernel/justification.h"
 #include "kernel/metavar.h"
 
 namespace lean {
-void justification_cell::add_pos_info(format & r, optional<expr> const & e, pos_info_provider const * p) {
+format to_pos(optional<expr> const & e, pos_info_provider const * p) {
     if (!p || !e)
-        return;
+        return format();
     format f = p->pp(*e);
     if (!f)
-        return;
-    r += f;
-    r += space();
+        return format();
+    return f + space();
 }
 
-format justification_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children,
-                              optional<metavar_env> const & menv) const {
-    format r;
-    add_pos_info(r, get_main_expr(), p);
-    r += pp_header(fmt, opts, menv);
-    if (display_children) {
-        buffer<justification_cell *> children;
-        get_children(children);
-        unsigned indent = get_pp_indent(opts);
-        for (justification_cell * child : children) {
-            r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children, menv)));
-        }
+typedef uint64 approx_set;
+static approx_set mk_empty_set() { return 0; }
+static approx_set mk_union(approx_set s1, approx_set s2) { return s1 | s2; }
+static approx_set mk_intersection(approx_set s1, approx_set s2) { return s1 & s2; }
+static approx_set mk_singleton(unsigned i) { return static_cast<uint64>(1) << (i % 64); }
+static approx_set may_contain(approx_set s, unsigned i) { return mk_intersection(s, mk_singleton(i)) != 0ull; }
+
+enum class justification_kind { Asserted, Composite, ExtComposite, Assumption, ExtAssumption };
+
+approx_set get_approx_assumption_set(justification const & j);
+
+struct justification_cell {
+    MK_LEAN_RC();
+    justification_kind m_kind;
+    void dealloc();
+    justification_cell(justification_kind k):m_rc(0), m_kind(k) {}
+    bool is_asserted() const { return m_kind == justification_kind::Asserted; }
+    bool is_assumption() const { return m_kind == justification_kind::Assumption || m_kind == justification_kind::ExtAssumption; }
+    bool is_composite() const { return m_kind == justification_kind::Composite || m_kind == justification_kind::ExtComposite; }
+    bool is_ext_assumption() const { return m_kind == justification_kind::ExtAssumption; }
+    bool is_ext_composite() const { return m_kind == justification_kind::ExtComposite; }
+};
+
+struct asserted_cell : public justification_cell {
+    pp_jst_fn      m_fn;
+    optional<expr> m_expr;
+    asserted_cell(pp_jst_fn const & fn, optional<expr> const & e):
+        justification_cell(justification_kind::Asserted),
+        m_fn(fn), m_expr(e) {}
+};
+
+struct composite_cell : public justification_cell {
+    approx_set    m_assumption_set; // approximated set of assumptions contained in child1 and child2
+    justification m_child[2];
+    composite_cell(justification_kind k, justification const & j1, justification const & j2):
+        justification_cell(k) {
+        m_child[0] = j1;
+        m_child[1] = j2;
+        m_assumption_set = mk_union(get_approx_assumption_set(j1), get_approx_assumption_set(j2));
     }
-    return r;
+    composite_cell(justification const & j1, justification const & j2):
+        composite_cell(justification_kind::Composite, j1, j2) {}
+};
+
+struct ext_composite_cell : public composite_cell {
+    pp_jst_fn      m_fn;
+    optional<expr> m_expr;
+    ext_composite_cell(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & e):
+        composite_cell(justification_kind::ExtComposite, j1, j2),
+        m_fn(fn),
+        m_expr(e) {}
+};
+
+struct assumption_cell : public justification_cell {
+    unsigned m_idx;
+    assumption_cell(justification_kind k, unsigned idx):
+        justification_cell(k), m_idx(idx) {}
+    assumption_cell(unsigned idx):
+        assumption_cell(justification_kind::Assumption, idx) {}
+};
+
+struct ext_assumption_cell : public assumption_cell {
+    pp_jst_fn      m_fn;
+    optional<expr> m_expr;
+    ext_assumption_cell(unsigned idx, pp_jst_fn const & fn, optional<expr> const & e):
+        assumption_cell(justification_kind::ExtAssumption, idx),
+        m_fn(fn),
+        m_expr(e) {}
+};
+
+asserted_cell * to_asserted(justification_cell * j) { lean_assert(j && j->is_asserted()); return static_cast<asserted_cell*>(j); }
+assumption_cell * to_assumption(justification_cell * j) { lean_assert(j && j->is_assumption()); return static_cast<assumption_cell*>(j); }
+ext_assumption_cell * to_ext_assumption(justification_cell * j) { lean_assert(j && j->is_ext_assumption()); return static_cast<ext_assumption_cell*>(j); }
+composite_cell * to_composite(justification_cell * j) { lean_assert(j && j->is_composite()); return static_cast<composite_cell*>(j); }
+ext_composite_cell * to_ext_composite(justification_cell * j) { lean_assert(j && j->is_composite()); return static_cast<ext_composite_cell*>(j); }
+
+approx_set get_approx_assumption_set(justification const & j) {
+    justification_cell * it = j.raw();
+    if (!it)
+        return mk_empty_set();
+    switch (it->m_kind) {
+    case justification_kind::Asserted:
+        return mk_empty_set();
+    case justification_kind::Assumption: case justification_kind::ExtAssumption:
+        return mk_singleton(to_assumption(it)->m_idx);
+    case justification_kind::Composite: case justification_kind::ExtComposite:
+        return to_composite(it)->m_assumption_set;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-bool justification::has_children() const {
-    buffer<justification_cell *> r;
-    get_children(r);
-    return !r.empty();
-}
-format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
-                         bool display_children, optional<metavar_env> const & menv) const {
-    lean_assert(m_ptr);
-    return m_ptr->pp(fmt, opts, p, display_children, menv);
-}
-format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const {
-    lean_assert(m_ptr);
-    return m_ptr->pp(fmt, opts, p, display_children, optional<metavar_env>());
+void justification_cell::dealloc() {
+    switch (m_kind) {
+    case justification_kind::Asserted:         delete to_asserted(this); break;
+    case justification_kind::Assumption:       delete to_assumption(this); break;
+    case justification_kind::ExtAssumption:    delete to_ext_assumption(this); break;
+    case justification_kind::Composite:        delete to_composite(this); break;
+    case justification_kind::ExtComposite:     delete to_ext_composite(this); break;
+    }
 }
 
-assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {}
-void assumption_justification::get_children(buffer<justification_cell*> &) const {}
-optional<expr> assumption_justification::get_main_expr() const { return none_expr(); }
-format assumption_justification::pp_header(formatter const &, options const &, optional<metavar_env> const &) const {
-    return format{format("Assumption"), space(), format(m_idx)};
-}
-
-
-bool depends_on(justification const & t, justification const & d) {
+bool depends_on(justification const & j, unsigned i) {
+    if (!may_contain(get_approx_assumption_set(j), i))
+        return false;
     buffer<justification_cell *>   todo;
-    buffer<justification_cell *>   children;
-    todo.push_back(t.raw());
+    todo.push_back(j.raw());
     while (!todo.empty()) {
         justification_cell * curr = todo.back();
         todo.pop_back();
-        if (curr == d.raw()) {
-            return true;
-        } else {
-            children.clear();
-            curr->get_children(children);
-            for (justification_cell * child : children) {
-                todo.push_back(child);
+        switch (curr->m_kind) {
+        case justification_kind::Asserted:
+            break;
+        case justification_kind::Assumption: case justification_kind::ExtAssumption:
+            if (to_assumption(curr)->m_idx == i)
+                return true;
+            break;
+        case justification_kind::Composite: case justification_kind::ExtComposite:
+            for (unsigned i = 0; i < 2; i++) {
+                justification c = to_composite(curr)->m_child[i];
+                if (may_contain(get_approx_assumption_set(c), i))
+                    todo.push_back(c.raw());
             }
         }
     }
     return false;
 }
+
+justification const & composite_child1(justification const & j) {
+    lean_assert(j.is_composite());
+    return to_composite(j.raw())->m_child[0];
+}
+
+justification const & composite_child2(justification const & j) {
+    lean_assert(j.is_composite());
+    return to_composite(j.raw())->m_child[0];
+}
+
+unsigned assumption_idx(justification const & j) {
+    lean_assert(j.is_assumption());
+    return to_assumption(j.raw())->m_idx;
+}
+
+justification::justification():m_ptr(nullptr) {}
+justification::justification(justification_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
+justification::justification(justification const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+justification::justification(justification && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+justification::~justification() { if (m_ptr) m_ptr->dec_ref(); }
+bool justification::is_none() const { return m_ptr == nullptr; }
+bool justification::is_asserted() const { return m_ptr && m_ptr->is_asserted(); }
+bool justification::is_assumption() const { return m_ptr && m_ptr->is_assumption(); }
+bool justification::is_composite() const { return m_ptr && m_ptr->is_composite(); }
+justification & justification::operator=(justification const & s) { LEAN_COPY_REF(s); }
+justification & justification::operator=(justification && s) { LEAN_MOVE_REF(s); }
+optional<expr> justification::get_main_expr() const {
+    justification_cell * it = m_ptr;
+    while (true) {
+        if (!it)
+            return none_expr();
+        switch (it->m_kind) {
+        case justification_kind::Asserted:
+            return to_asserted(it)->m_expr;
+        case justification_kind::ExtAssumption:
+            return to_ext_assumption(it)->m_expr;
+        case justification_kind::ExtComposite:
+            return to_ext_composite(it)->m_expr;
+        case justification_kind::Assumption:
+            return none_expr();
+        case justification_kind::Composite:
+            it = to_composite(it)->m_child[0].raw();
+            break;
+        }
+    }
+}
+format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s) {
+    justification_cell * it = m_ptr;
+    while (true) {
+        if (!it)
+            return format();
+        switch (it->m_kind) {
+        case justification_kind::Asserted:
+            return to_asserted(it)->m_fn(fmt, opts, p, s);
+        case justification_kind::ExtAssumption:
+            return to_ext_assumption(it)->m_fn(fmt, opts, p, s);
+        case justification_kind::ExtComposite:
+            return to_ext_composite(it)->m_fn(fmt, opts, p, s);
+        case justification_kind::Assumption:
+            return format(format("Assumption "), format(to_assumption(it)->m_idx));
+        case justification_kind::Composite:
+            it = to_composite(it)->m_child[0].raw();
+            break;
+        }
+    }
+}
+
+justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s) {
+    return justification(new ext_composite_cell(j1, j2, fn, s));
+}
+justification mk_composite1(justification const & j1, justification const & j2) {
+    return justification(new composite_cell(j1, j2));
+}
+justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s) {
+    return justification(new ext_assumption_cell(idx, fn, s));
+}
+justification mk_assumption_justification(unsigned idx) {
+    return justification(new assumption_cell(idx));
+}
+justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s) {
+    return justification(new asserted_cell(fn, s));
+}
+justification mk_justification(pp_jst_sfn const & fn, optional<expr> const & s) {
+    return mk_justification([=](formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & subst) {
+            return compose(to_pos(s, p), fn(fmt, opts, subst));
+        }, s);
+}
 }
diff --git a/src/kernel/justification.h b/src/kernel/justification.h
index 466abf9a6..77b914fef 100644
--- a/src/kernel/justification.h
+++ b/src/kernel/justification.h
@@ -15,87 +15,121 @@ Author: Leonardo de Moura
 #include "kernel/pos_info_provider.h"
 
 namespace lean {
-class metavar_env;
-class justification;
-/**
-   \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 justification_cell {
-    MK_LEAN_RC();
-    void dealloc() { delete this; }
-protected:
-    static void add_pos_info(format & r, optional<expr> const & e, pos_info_provider const * p);
-public:
-    justification_cell():m_rc(0) {}
-    virtual ~justification_cell() {}
-    virtual format pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const = 0;
-    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
-                      bool display_children, optional<metavar_env> const & menv) const;
-    virtual void get_children(buffer<justification_cell*> & r) const = 0;
-    virtual optional<expr> get_main_expr() const { return none_expr(); }
-    bool is_shared() const { return get_rc() > 1; }
-};
+class substitution;
+struct justification_cell;
 
 /**
-   \brief Base class for justification objects used to justify case-splits.
+   \brief When a set of constraints cannot be solved, we must print some "error" message to the user.
+   The pp_jst_fn is a generic funciton that produces these messages. We can associate these functions
+   to justification objects.
 */
-class assumption_justification : public justification_cell {
-    unsigned m_idx;
-public:
-    assumption_justification(unsigned idx);
-    virtual void get_children(buffer<justification_cell*> &) const;
-    virtual optional<expr> get_main_expr() const;
-    virtual format pp_header(formatter const &, options const &, optional<metavar_env> const & menv) const;
-};
+typedef std::function<format(formatter const &, options const &, pos_info_provider const *, substitution const &)> pp_jst_fn;
 
 /**
-   \brief Smart pointer for justification_cell's
+    \brief Objects used to justify unification (and level) constraints and metavariable assignments.
+
+    There are 4 basic kinds of justification:
+    - None:       the null justification.
+    - Asserted:   a justification produced by the type checker.
+    - Assumption: for case-splits inside the elaborator and other constraint solvers.
+    - Composite:  the combination of two other justification objects.
+
+    A composite justification is used, for example, to justify a constraint produced by
+    replacing a metavariable ?M by its assignment in a constraint C.
 */
 class justification {
     justification_cell * m_ptr;
+    justification(justification_cell * ptr);
 public:
-    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(); }
-
-    explicit operator bool() const { return m_ptr != nullptr; }
-
-    justification_cell * raw() const { return m_ptr; }
+    justification();
+    justification(justification const & s);
+    justification(justification && s);
+    ~justification();
 
     friend void swap(justification & a, justification & b) { std::swap(a.m_ptr, b.m_ptr); }
 
-    justification & operator=(justification const & s) { LEAN_COPY_REF(s); }
-    justification & operator=(justification && s) { LEAN_MOVE_REF(s); }
-    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
-              bool display_children, optional<metavar_env> const & menv) const;
-    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const;
-    optional<expr> get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : none_expr(); }
-    void get_children(buffer<justification_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
-    bool has_children() const;
+    bool is_none() const;
+    bool is_asserted() const;
+    bool is_assumption() const;
+    bool is_composite() const;
+
+    justification_cell * raw() const { return m_ptr; }
+
+    justification & operator=(justification const & s);
+    justification & operator=(justification && s);
+    /**
+       \brief Convert this justification into a format object. This method is usually used to report
+       "error" messages to users.
+    */
+    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s);
+    /**
+       \brief Return an expression associated with the justification object.
+    */
+    optional<expr> get_main_expr() const;
+
+    friend justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s);
+    friend justification mk_composite1(justification const & j1, justification const & j2);
+    friend justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s);
+    friend justification mk_assumption_justification(unsigned idx);
+    friend justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s);
 };
 
-inline justification mk_assumption_justification(unsigned idx) { return justification(new assumption_justification(idx)); }
+/**
+   \brief Simplifer version of pp_jst_fn
+*/
+typedef std::function<format(formatter const &, options const &, substitution const &)> pp_jst_sfn;
+
+/** \brief Return a format object containing position information for the given expression (if available) */
+format to_pos(optional<expr> const & e, pos_info_provider const * p);
 
 /**
-   \brief Return true iff \c t depends on \c d.
-   That is \c t is a descendant of \c d.
+   \brief Combine the two given justifications into a new justification object, and use
+   the given function to convert the justification into a format object.
 */
-bool depends_on(justification const & t, justification const & d);
+justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s);
+/**
+   \brief Similar to \c mk_composite, but uses \c j1.pp to convert the
+   resulting justification into a format object.
+*/
+justification mk_composite1(justification const & j1, justification const & j2);
+/**
+   \brief Alias for \c mk_composite1
+*/
+justification mk_substitution_justification(justification const & j1, justification const & j2);
+/**
+   \brief Create a "case-split" justification with the given \c idx.
+*/
+justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s);
+/**
+   \brief Similar to the previous function, but fn just returns the format object "assumption idx", and s is the none.
+*/
+justification mk_assumption_justification(unsigned idx);
+/**
+   \brief Create a justification for constraints produced by the type checker.
+*/
+justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s);
+/**
+   \brief Create a justification for constraints produced by the type checker.
+   It is similar to the previous function, but the position of \c s will be automatically included.
+*/
+justification mk_justification(pp_jst_sfn const & fn, optional<expr> const & s);
 
-/** \brief Add \c t to \c r */
-inline void push_back(buffer<justification_cell*> & r, justification const & t) {
-    if (t) r.push_back(t.raw());
-}
+/**
+   \brief Return the first child of a composite justification.
+   \pre j.is_composite()
+*/
+justification const & composite_child1(justification const & j);
+/**
+   \brief Return the second child of a composite justification.
+   \pre j.is_composite()
+*/
+justification const & composite_child2(justification const & j);
+/**
+   \brief Return the index of an assumption justification.
+   \pre j.is_assumption()
+*/
+unsigned assumption_idx(justification const & j);
 
-/** \brief Add justifications in the collection \c s into r. */
-template<typename T>
-void append(buffer<justification_cell*> & r, T const & s) {
-    for (auto t : s)
-        push_back(r, t);
-}
+/** \brief Return true iff \c j depends on the assumption with index \c i. */
+bool depends_on(justification const & j, unsigned i);
 }
diff --git a/src/kernel/pos_info_provider.h b/src/kernel/pos_info_provider.h
index 692e5a14a..5b751bfb5 100644
--- a/src/kernel/pos_info_provider.h
+++ b/src/kernel/pos_info_provider.h
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 /**
-   \brief Abstract class for providing expression position information (line number and position).
+   \brief Abstract class for providing expression position information (line number and column).
 */
 class pos_info_provider {
 public:
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 1a6bc6c1b..ee49b07f9 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -419,6 +419,7 @@ int main() {
     std::cout << "sizeof(expr_cell):       " << sizeof(expr_cell) << "\n";
     std::cout << "sizeof(optional<expr>):  " << sizeof(optional<expr>) << "\n";
     std::cout << "sizeof(optional<sexpr>): " << sizeof(optional<sexpr>) << "\n";
+    std::cout << "sizeof(std::function):   " << sizeof(std::function<expr(expr const &, optional<expr> const &)>) << "\n";
     std::cout << "done" << "\n";
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp
index acae8ff2d..7b6f33b18 100644
--- a/src/tests/util/format.cpp
+++ b/src/tests/util/format.cpp
@@ -116,11 +116,16 @@ static void tst4() {
     lean_assert_eq(s.str(), "() (foo bar) nil \"test\" (100 1/2)");
 }
 
+static void tst5() {
+    std::cout << "{" << format() << "}" << "\n";
+}
+
 int main() {
     save_stack_info();
     tst1();
     tst2();
     tst3();
     tst4();
+    tst5();
     return has_violations() ? 1 : 0;
 }