diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean
index ede9f6346e..89da065dbd 100644
--- a/src/Lean/Compiler/LCNF/Types.lean
+++ b/src/Lean/Compiler/LCNF/Types.lean
@@ -173,9 +173,7 @@ where
       | _ => return anyExpr
     let mut result := fNew
     for arg in args do
-      if (← isProp arg) then
-        result := mkApp result erasedExpr
-      else if (← isPropFormer arg) then
+      if ← isProp arg <||> isPropFormer arg then
         result := mkApp result erasedExpr
       else if (← isTypeFormer arg) then
         result := mkApp result (← toLCNFType arg)