IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ncompose wf121 1. 'a : Type
2. f : 'a'a 3. n : 4. 0<n 5. x:'a. ncompose(f;n-1;x) 'a 6. x : 'a 7. n=0
ncompose(f;n-1;x) 'a
By:
BackThru 5
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a
x:'a. ncompose(f;n-1;x) 
'a
n=
0
ncompose(f;n-1;x) 
