diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index fa9e3b0bf0..407174a33a 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -846,10 +846,7 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      -- Remark: we should consider using `pure view.kind.isTheorem <||> isProp header.type`, and
-      -- also handle definitions. We used the following approach because it is less disruptive to Mathlib.
-      -- Moreover, the type of most definitions are not propositions anyway.
-      if ← pure view.kind.isTheorem <||> (pure view.kind.isExample <&&> isProp header.type) then
+      if ← pure view.kind.isTheorem <||> isProp header.type then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 445a458daa..680b9c24f7 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/tests/lean/autoPPExplicit.lean.expected.out
@@ -5,4 +5,4 @@ argument
 has type
   Prop : Type
 but is expected to have type
-  α : Sort ?u
+  α : Sort u_1