f:(). (i:. 0i  f(i) = i2) & (i:. 0i  f(i) = (-i)2-1)

By:	Witness: i.if 0i i2 else (-i)2-1 fi with type  THEN Reduce Concl

1	(i.if 0i i2 else (-i)2-1 fi)	2 steps
2	1. (i.if 0i i2 else (-i)2-1 fi)   2. i :  3. 0i   if 0i i2 else (-i)2-1 fi = i2	1 step
3	1. (i.if 0i i2 else (-i)2-1 fi)   2. i :  3. 0i   if 0i i2 else (-i)2-1 fi = (-i)2-1	1 step

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