(5steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc predicativity sample8 1 2

1. f : 
2. n:f(n) = 0
3. n : 
  if f(n)=0 False else C:Prop. C fi  Prop


By: Inst: n:f(n) = 0 Using:[n]


Generated subgoal:

1 4. f(n) = 0
  if f(n)=0 False else C:Prop. C fi  Prop

1 step

About:
ifthenelseintnatural_numberapply
functionequalmemberpropfalse
all
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(5steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc