IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ncompose wf111 1. 'a : Type
2. f : 'a'a 3. x : 'a if 0=0 then x else f(ncompose(f;0-1;x)) fi 'a
By:
Unfold `bif` 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a
if 0=
0 then x else f(ncompose(f;0-1;x)) fi 
'a
