This question is basically a request for clarification about a remark made by Sam Sanders [in a comment](https://mathoverflow.net/questions/455834/proof-of-global-peano-existence-theorem-in-zf#comment1180607_455834) to another question: IIUC what he's saying, there are statements that can be proved *either* with a small amount of Choice (like, countable choice) and then in a very weak framework from the Comprehension point of view (e.g., $\mathsf{WLK}_0$), *or* without Choice but then with a strong amount of Comprehension, but not without Choice and with weak Comprehension.

I'd like to know more about such statements, what the intuition between this “Choice for Comprehension” tradeoff is, and how this is proved (or where I might learn more about them).

Please be liberal in understanding the question: classical reverse math, constructive¹ reverse math, set theory, anything in the direction of “trading Choice for some non-choicy set-building operation” is interesting.  Are there interesting² statements that can be proved in weak subsystems of $\mathsf{ZFC}$ (like $\mathsf{KPC}$), or in full $\mathsf{ZF}$, but not in their intersection (like $\mathsf{KP}$), for example?

1. I am aware of some things that go slightly in that direction, like the equality of Cauchy and Dedekind reals can be proved in $\mathsf{IZF}$ with Countable Choice or in classical $\mathsf{ZF}$ (without any Choice).  But this is a “Choice for Omniscience” tradeoff which is a bit different from what I'm asking.

2. Please don't point out that the logical disjunction between the axiom of choice and some strong comprehension/replacement axiom works, or any such obviously artificial example.