diff --git a/src/lean.ml b/src/lean.ml
index 429b9c0..9bad8c6 100644
--- a/src/lean.ml
+++ b/src/lean.ml
@@ -1019,7 +1019,7 @@ and declare_ind n { params; ty; ctors; univs } i =
       in
       assert (
         squashy.lean_squashes
-        || (Global.lookup_mind mind).mind_packets.(0).mind_kelim == InType);
+        || (Global.lookup_mind mind).mind_packets.(0).mind_squashed == None);
       (mind, algs, ind_name, cnames, univs, squashy)
   in