Nuprl - Proof: factorial via iter wf 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial via iter wf 1 1

1. k :

k!k = 0

By:	Def of k!k

Generated subgoal:

1 ( i:{k-k..k}. i+1) = 0
4 steps

About:

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