1. 'a : S
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)))

1

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

6 steps

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