perf: prove `String` literal disequalities in `match` equations without `String.decEq` (#16354)

This PR speeds up the generation of equation lemmas for definitions that
`match` on `String` literals. With 64 literal patterns, generation used
to hit the heartbeat limit.

The equation generators try `rfl` first, which reduces `String.decEq` on
the literals. This PR adds `Meta.Config.stringLitToCtor`. When it is
`false`, `whnf` and `isDefEq` throw an internal exception instead of
converting a `String` literal into a constructor application.
`proveCondEqThm` and `mkEqnProof` try `rfl` with the flag off, then the
proof that does not use `rfl`, then unrestricted `rfl`.

Part of #16313.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>