I'm trying to work through two (non-assessed) class-work questions and am stuck on a question that seems similar to one I could do.The first question was to prove that there does not exist a $\lambda$-term $f$ that, given two $\lambda$-terms $m$ and $n$, can determine whether or not they are $\beta$-equivalent  i.e. there is no $f$ such that $\lambda\beta \vdash f \ m \ n = \textbf{t}$ if $m \ =_\beta \ n$ and $\lambda\beta \vdash f \ m \ n = \textbf{f}$ if $m \ \neq_\beta \ n$. I think I have done this relatively easily by appealing to the Scott-Curry theorem.I'm now stuck on proving the same but for $m, n$ being in normal form. If I try to use the Scott-Curry theorem, showing that the set $A = \{ x = m \mid x \mbox{ in normal form} \}$ is inseparable, so that no $g \equiv f \ m$ can exist, then I cannot show that $A$ is closed under $\beta$-equality, which we require to apply the Scott-Curry theorem. So I don't think this is the correct approach.Could anyone give me some help on how to formally prove this? I've played around with contexts, Bhm's theorem, etc. I feel like the fact $m, n$ are not required to be closed is important?
Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus
lo.logic;computability;pl.programming languages;lambda calculus