For example, if your order of proof enumeration is unlucky enough, you could find U'="return 1000" with no dependence on A at all, then two-box and make that equation true.

I wonder if reflection on your own inference system could make things like this go away...