diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index dc090940b2..5b4541d54c 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -262,6 +262,13 @@ struct structure_cmd_fn {
             } else {
                 if (has_placeholder(m_type))
                     throw_explicit_universe(pos);
+                // Note that if we do infer the result universe, `mk_result_level` will ensure that the
+                // result type cannot be zero when the structure might otherwise eliminate only to zero.
+                if (m_env.impredicative() && !is_zero(sort_level(m_type)) && !is_not_zero(sort_level(m_type)))
+                    throw parser_error("invalid universe polymorphic structure declaration, "
+                                       "the resultant universe is not Prop (i.e., 0), "
+                                       "but it may be Prop for some parameter values "
+                                       "(solution: use 'l+1' or 'max 1 l')", m_p.pos());
             }
         } else {
             if (!m_infer_result_universe)
diff --git a/tests/lean/bad_structures.lean.expected.out b/tests/lean/bad_structures.lean.expected.out
index 9f0c43ff94..4881671cc3 100644
--- a/tests/lean/bad_structures.lean.expected.out
+++ b/tests/lean/bad_structures.lean.expected.out
@@ -1,2 +1,3 @@
 bad_structures.lean:1:71: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
 bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
+bad_structures.lean:7:60: error: invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')
diff --git a/tests/lean/structure_result_type_may_be_zero.lean b/tests/lean/structure_result_type_may_be_zero.lean
new file mode 100644
index 0000000000..b002fd6684
--- /dev/null
+++ b/tests/lean/structure_result_type_may_be_zero.lean
@@ -0,0 +1 @@
+record Fun.{uA uB} (A : Type.{uA}) (B : Type.{uB}) : Type.{imax uA uB} := (item : Π(a : A), B)
diff --git a/tests/lean/structure_result_type_may_be_zero.lean.expected.out b/tests/lean/structure_result_type_may_be_zero.lean.expected.out
new file mode 100644
index 0000000000..0163c41c31
--- /dev/null
+++ b/tests/lean/structure_result_type_may_be_zero.lean.expected.out
@@ -0,0 +1 @@
+structure_result_type_may_be_zero.lean:1:71: error: invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')