'a:S. 
  equal
  (cond
  ,t:hbool. t1:'a. t2:'a. select
  ,t:hbool. t1:'a. t2:'a. (x:'a. and
  ,t:hbool. t1:'a. t2:'a. (x:'a. (implies(equal(t,t),equal(x,t1))
  ,t:hbool. t1:'a. t2:'a. (x:'a. ,implies(equal(t,f),equal(x,t2)))))

1

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)))

8 steps

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