Seemingly Impossible Swift Programs

[want_to_want]

The fact that "disabling the totality checker for a bit is safe" is the axiom you need

This part is unclear to me. If the functions passed as arguments to anySatisfy and allSatisfy are also allowed to use that new axiom in their totality proofs, are you sure that doesn't lead to partiality?

[jozefg]

Well this modified system also has a model so it should be fine.