chore(*): remove uses of with_cases (#16894)
For the port, resolves #16568.
I did a pretty crude job, so the proofs are likely more brittle and ugly than before, but at least for the `rbtree` file it doesn't seem anoyone really needs to read these proofs often.
One fun side-effect of this is that the linter started complaining about unused arguments, so we fix those too.
