Nuprl Basics - Proof: sfa doc factbody polytyping 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc factbody polytyping 1

1. k :

2. f :

3. x :

(k+1)

if x=

1 else x

f(x-1) fi

By:	SplitOnConclITE

Generated subgoal:

1 4. x = 0
xf(x-1)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html