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

By:	Unab [`bchoose`] THEN LemmaRW Thm* P:('aType), x:'a. P(x)  (y:'a. P(y)  x = y)  (@y:'a. P(y)) = x

1

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

5 steps

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