decide +kernel on a big conjunction gets killed (exit 137, no message): split it

A decide +kernel proof of an 11-part decidable Valid predicate on a 60-vertex/32-face table made lean exit with code 137 after ~40 s and print nothing (container memory cap 6 GB; lake env lean just looks like it succeeded with empty output, so check the exit code, or use lake build, which reports it). Each conjunct on its own took 2-15 s. Fix: unfold Valid; exact ⟨by decide +kernel, by decide +kernel, ...⟩ with one decide per conjunct; the kernel no longer keeps one giant shared reduction. Then elaboration of the 11 instances together goes over 200000 heartbeats, so put set_option maxHeartbeats 1000000 in before the docstring (putting it between the docstring and theorem is a parse error). To find the expensive part, generate one test file per conjunct with the others sorry.