diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 38fe26e6d..2ae1129d0 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -200,21 +200,21 @@ void type_checker::check_level(level const & l, expr const & s) {
 app_delayed_justification::app_delayed_justification(environment const & env, expr const & e, expr const & f_type, expr const & a_type):
     m_env(env), m_e(e), m_fn_type(f_type), m_arg_type(a_type) {}
 
+justification mk_app_justification(environment const & env, expr const & e, expr const & d_type, expr const & a_type) {
+    auto pp_fn = [=](formatter const & fmt, options const & o, substitution const & subst) {
+        return pp_app_type_mismatch(fmt, env, o,
+                                    subst.instantiate_metavars_wo_jst(e),
+                                    subst.instantiate_metavars_wo_jst(d_type),
+                                    subst.instantiate_metavars_wo_jst(a_type));
+    };
+    return mk_justification(e, pp_fn);
+}
+
 justification app_delayed_justification::get() {
     if (!m_jst) {
         // We should not have a reference to this object inside the closure.
         // So, we create the following locals that will be captured by the closure instead of 'this'.
-        environment env = m_env;
-        expr e          = m_e;
-        expr fn_type    = m_fn_type;
-        expr arg_type   = m_arg_type;
-        m_jst = mk_justification(e,
-                                 [=](formatter const & fmt, options const & o, substitution const & subst) {
-                                     return pp_app_type_mismatch(fmt, env, o,
-                                                                 subst.instantiate_metavars_wo_jst(e),
-                                                                 subst.instantiate_metavars_wo_jst(binding_domain(fn_type)),
-                                                                 subst.instantiate_metavars_wo_jst(arg_type));
-                                 });
+        m_jst = mk_app_justification(m_env, m_e, binding_domain(m_fn_type), m_arg_type);
     }
     return *m_jst;
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 8452cdfc5..cc90a1b6c 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -151,6 +151,12 @@ certified_declaration check(environment const & env, declaration const & d,
                             name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true);
 certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque = name_set(), bool memoize = true);
 
+/**
+    \brief Create a justification for an application \c e where the expected type must be \c d_type and
+    the argument type is \c a_type.
+*/
+justification mk_app_justification(environment const & env, expr const & e, expr const & d_type, expr const & a_type);
+
 /**
    \brief Create a justification for a application type mismatch,
    \c e is the application, \c fn_type and \c arg_type are the function and argument type.