chore: fixes spurious omega error in #5315

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -422,10 +422,11 @@ partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) :
     trace[omega] "adding fact: {t}"
     match t with
     | .forallE _ x y _ =>
-      if (← isProp x) && (← isProp y) then
+      if ← pure t.isArrow <&&> isProp x <&&> isProp y then
         p.addFact (mkApp4 (.const ``Decidable.not_or_of_imp []) x y
           (.app (.const ``Classical.propDecidable []) x) h)
       else
+        trace[omega] "rejecting forall: it's not an arrow, or not propositional"
         return (p, 0)
     | .app _ _ =>
       match_expr t with

tests/lean/run/omega.lean

@@ -506,6 +506,54 @@ example
     n = 65536 := by
   bv_omega
 
+-- From https://github.com/leanprover/lean4/issues/5315
+-- This used to fail with an unexpected bound variable error.
+
+def simple_foldl (f: β → α → β) (a: Array α) (i: Nat) (b: β): β :=
+  if h: i < a.size then
+    simple_foldl f a (i+1) (f b a[i])
+  else
+    b
+
+/--
+error: omega could not prove the goal:
+No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
+-/
+#guard_msgs in
+theorem simple_fold_monotonic₁ (a: Array α) (f: β → α → β) (i: Nat) {P: α → β → Prop} {x: α}
+  (base: P x b)
+  (mono: ∀ x x' y, P x y → P x (f y x')): P x (simple_foldl f a i b) := by
+    unfold simple_foldl
+    split <;> try trivial
+    apply simple_fold_monotonic₁
+    . apply mono; exact base
+    . exact mono
+  termination_by a.size - i
+  decreasing_by
+    exfalso
+    rename_i a b
+    clear a b mono base
+    rename_i a; clear a
+    clear base
+    clear x
+    rename_i a; clear a
+    clear x
+    clear P
+    rename_i a; clear a
+    clear P
+    clear i
+    rename_i a; clear a
+    clear i
+    clear f
+    rename_i a; clear a
+    clear f
+    clear a
+    rename_i a; clear a
+    clear a
+    clear b
+    rename_i a
+    omega
+
 /-! ### Error messages -/
 
 /--