Wow, this must be one of the most advanced questions in this section. I am not a specialist on epsilon-calculus, but I'll give it a try.

So , where means "syntactically equal". Therefore, we need to prove . Note that semantically, must return the same answer in both occurrences; if returned some random witness of every time it is called, the formula we need is not necessarily true. In other words, is deterministic, just like regular functional symbols.

The structure of the proof is probably similar to that of the proof with . I.e., we consider two cases: and . In the first case we take the witness of and conclude , and therefore . The second case is similar.

So, from we conclude . Next, according to the plan, we need to derive . This is possible using the axiom about .