I'm working through Simon Peyton Jones' The Implementation of Functional Programming Languages and on page 20 I see:IF TRUE ((λp.p) 3) ↔ IF TRUE 3         (per β red)   (1)                   ↔ (λx.IF TRUE 3 x)  (per η red)   (2)                   ↔ (λx.3)                          (3)Step 1 to 2 is explained as η-conversion. But from 2 to 3 it says The final step is the reduction rule for IF. I'm not sure what this reduction rule is. 
Reduction rule for IF?
logic;programming languages;lambda calculus;term rewriting;operational semantics