IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mu-property12 1. f : 2. n : 3. n0
4. f(n)
5. f(0)
f(mu(x.f(x+1))+1) & (i:. i<mu(x.f(x+1))+1 f(i))
By:
Subst' (n = 0) -2
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html