Thank you again!

Thanks for the feedback, @EmilJeřábek! I am not sure I understand the intuition though, so remind me: is there a reduction theorem that says if a statement can be formalized in $APC_2$ and a proof of the statement exists (say, in ZFC), then a proof can be also be given in a much weaker system? I recall a theorem of that kind but I cannot pinpoint it.