From 713a46cd75a813a501ef5acd8eee29c8a99abdd5 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 4 Aug 2025 21:13:02 -0700
Subject: [PATCH] chore: adopt `<||>` to reduce code duplication (#9719)

---
 src/Lean/Compiler/LCNF/Types.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

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)