Lean: Slow performance for constructor247 test

[Alasdair]

This test was originally implemented to make sure we don't run into OCaml's limitation of 246 constructors in a datatype, but it's a good stress test for prover backends. Currently on my local machine this test causes lean to hang, but it seems to be working in CI, which is a bit odd.