(19steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mu-property 1 2

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:
boolassertintnatural_numberaddless_thanlambdaapply
functionequalimpliesandall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(19steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc