Renaming a function's bound variables without changing its meaning (e.g. λx.x to λy.y)

A simplification rule where a function that does nothing but apply another expression to its argument can be replaced by that expression directly (e.g. λx.fx to f)

None of the options is correct.

Applying a function to its argument by substitution (e.g. (λx.x)y to y)

A rule that proves any lambda expression can be encoded as a number.