Commit 2025-11-20 14:55 6bbd26f0
View on Github →feat: add splitOnP_append_cons (#31825)
This PR adds a lemma for splitOnP, allowing expressions where a splitOnP on a concatenation to be better simplified. Also golfs a relevant consequence with the new lemma.
Related to https://github.com/google-deepmind/formal-conjectures/pull/1120