diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index ed5f63fa0..b7c924a47 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1291,7 +1291,19 @@ static environment congr_lemma_cmd(parser & p) {
     auto r = cm.mk_congr_simp(e);
     if (!r)
         throw parser_error("failed to generated congruence lemma", pos);
-    p.regular_stream() << r->get_proof() << "\n:\n" << r->get_type() << "\n";;
+    auto out = p.regular_stream();
+    out << "[";
+    bool first = true;
+    for (auto k : r->get_arg_kinds()) {
+        if (!first) out << ", "; else first = false;
+        switch (k) {
+        case congr_lemma_manager::congr_arg_kind::Fixed: out << "fixed"; break;
+        case congr_lemma_manager::congr_arg_kind::Eq:    out << "eq";    break;
+        case congr_lemma_manager::congr_arg_kind::Cast:  out << "cast";  break;
+        }
+    }
+    out << "]\n";
+    out << r->get_proof() << "\n:\n" << r->get_type() << "\n";;
     type_checker tc(env);
     expr type = tc.check(r->get_proof(), ls).first;
     if (!tc.is_def_eq(type, r->get_type()).first)
diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp
index e63726b73..389967ee7 100644
--- a/src/library/congr_lemma_manager.cpp
+++ b/src/library/congr_lemma_manager.cpp
@@ -95,10 +95,6 @@ class congr_lemma_manager::imp {
     }
 
     optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
-        for (unsigned i = 0; i < kinds.size(); i++)
-            std::cout << (unsigned)kinds[i] << " ";
-        std::cout << "\n";
-
         expr fn_type = whnf(infer(fn));
         name e_name("e");
         buffer<expr> lhss;
@@ -142,8 +138,6 @@ class congr_lemma_manager::imp {
                 eqs.push_back(none_expr());
                 break;
             }}
-            // std::cout << lhss.back() << "\n";
-            // std::cout << rhss.back() << "\n\n";
             fn_type  = whnf(instantiate(binding_body(fn_type), lhs));
         }
         expr lhs = mk_app(fn, lhss);