\(\lambda\mu\)-calculus and Böhm's theorem (Q2732290)

A closed lambda term \(M\) is solvable if there exist \(M_1, \ldots ,M_n\) such that \(MM_1\ldots M_n\;\beta\)-reduces to \(I\). Böhm's Theorem states that for any two closed lambda terms \(M\) and \(N\), if for all \(N_1, \ldots ,N_k, \;MN_1, \ldots ,N_k\) is solvable if and only if \(NN_1, \ldots ,N_k\) is solvable, then \(M\) is \(\eta\)-equal to \(N\). David and Py consider this theorem for Parigot's \(\lambda \mu\)-calculus, which is \(\lambda \)-calculus extended using a \(\mu\)-operator so that the types of the terms are classical \(\neg\to\) theorems. The \(\lambda \mu\)-calculus however is not Church-Rosser when \((\eta)\) is included. This problem has been overcome by Py by including an additional reduction rule that restores the Church-Rosser property. In this paper David and Py find a counterexample to Böhm's Theorem with this form of reduction.