Commit 2022-10-12 01:16 4d416710

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.