IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mu wf121 1. b : 2. 0<b 3. f:(). (n:. nb-1 & f(n)) mu(f) 4. f : 5. n : 6. nb 7. f(n)
8. f(0)
9. n = 0
mu(x.f(x+1))+1
By:
HypSubst' -1 -3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
f:(
). (
n:
b-1 & f(n)) 
mu(f) 
f(0)
mu(
x.f(x+1))+1 
