> Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...)
Actually, this is not true. f |n| could expand into \x. \y. (|n| args...) instead, where the args contain x and y. But the rest of your argument still applies to the application of |n|.
Actually, this is not true. f |n| could expand into \x. \y. (|n| args...) instead, where the args contain x and y. But the rest of your argument still applies to the application of |n|.