1. 'a : S
  (b:. p:'a. q:'a. if b then p else q fi )
  =
  (t:. t1:'a. t2:'a. @x:'a
  (t:. t1:'a. t2:'a. @((t = true)(x = t1)
  (t:. t1:'a. t2:'a. @(t = false)(x = t2)))

1

2. t :  3. t1 : 'a 4. t2 : 'a   if t then t1 else t2 fi    =   (@x:'a. ((t = true)(x = t1)(t = false)(x = t2)))

7 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html