From df113de72553bbb05bf4d6975fc0391c7f89cbfc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Jul 2016 10:37:27 -0700
Subject: [PATCH] fix(library/congr_lemma): compilation error in debug mode

---
 src/library/congr_lemma.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/library/congr_lemma.cpp b/src/library/congr_lemma.cpp
index 9ad719f2a3..81136eabe2 100644
--- a/src/library/congr_lemma.cpp
+++ b/src/library/congr_lemma.cpp
@@ -335,7 +335,6 @@ struct congr_lemma_manager {
             expr pr2 = mk_eq_refl(m_ctx, a);
             for (; i < kinds.size(); i++) {
                 if (kinds[i] == congr_arg_kind::Cast && !pinfos[i].is_prop()) {
-                    lean_assert(pinfos[i].is_subsingleton());
                     expr r1   = rhss1[i];
                     expr r2   = rhss[i];
                     expr r1_eq_r2 = mk_app(m_ctx, get_subsingleton_elim_name(), r1, r2);