Reduction rule for IF?
The reduction rule you ask for is the usual one for IF statements. It consists of two computation rules and one context rule:


  
  $\text{IF TRUE}$ $a$ $b$ $\to$ $a$ 
  $\text{IF FALSE}$ $a$ $b$ $\to$ $b$  
  $\dfrac{a\to a&#39;}{\text{IF}~a\ b\ c\to \text{IF}~a&#39;\ b\ c}$
  


In both the call-by-value (strict) and call-by-need (lazy) settings, both $a$ and $b$ can be arbitrary expressions. They need not be values.

Rules of this kind, that reduce specific functions (here IF), are often called delta rules.

Now, the reason step (2) above is necessary is so that the reduction rules for $\text{IF}$ can apply. $\text{IF}$ requires 3 arguments, but in the original term it has only two, so cannot be reduced. ($\text{IF}$ is being partially applied, just
like any function in Haskell. This means that only part of its arguments need to be supplied.) The use of $\eta$-expansion provides the additional argument, without changing the semantics.