\x.\y. (x y) can be rewritten to \x.x via eta-contraction, viz. the eta rule is
'M == \x.(M x)` when x does not appear free in M.
[Uh, been so long, hope I got that right.]
1 Like
\x.\y. (x y) can be rewritten to \x.x via eta-contraction, viz. the eta rule is
'M == \x.(M x)` when x does not appear free in M.
[Uh, been so long, hope I got that right.]