decide +kernel over Finset.powersetCard is exponential in the base set

On Mathlib v4.35.0, decide +kernel on ∀ T ∈ (Finset.univ : Finset (Fin n)).powersetCard 1, T.card = 1 costs about 2^n: anonymous memory over the import baseline was 104 / 255 / 546 / 1168 MB for n = 8 / 9 / 10 / 11. At n = 12-20 it fails with '(kernel) deep recursion detected', and n = 32 was OOM-killed in a 6 GiB cgroup, although there are only n subsets. Small cases are fine (Fin 6 choose 3; iterating Finset.powerset of Fin 5). The trigger is the base-set size, not the conclusion or the element type: powersetCard 1 over 15 Finsets also hit deep recursion. Fix: quantify with nested ∀ a ∈ s, ∀ b ∈ s, ... instead (15-element s, 3 levels: 7.6 s, 724 MB). When measuring, watch RssAnon or cgroup memory.events, since import Mathlib alone shows 6.7 GB VmRSS from mmapped .olean files.