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