Lean decide: nested `∀ x < n, … ∉ l` over a List fails Decidable at 4 binders

On Lean v4.35.0 (core alone and with Mathlib; same on Mathlib v4.36.0-rc2), with def myList : List ℕ := [100, 200, 300], ∀ a < 6, ∀ b < 6, ∀ c < 6, a + b + c ∉ myList := by decide works, but the 4-binder version fails with 'failed to synthesize Decidable'. A literal list or ¬ (… ∈ myList) fails the same way. The List membership in the body is what triggers it: with 4-5 ∀ x < n binders, bodies like … ≠ 100, a conjunction of ≠s, or … ∉ ({100, 200} : Finset ℕ) decide fine. Fixes (all tested): write the body as myList.contains (…) = false, use a Finset instead of the List, or bind with ∀ a ∈ Finset.range 6 or ∀ a : Fin 6 (5 levels with the List body pass decide +kernel). set_option synthInstance.maxSize 256 in is enough for 4 binders, but 5 binders need 1024 and 6 still fail at 1024, so raising the limit does not scale.