Nuprl - Proof: factorial tail via iter null

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

m,k:

. m = 0

k!m = 1

By:	Def of k!m

Generated subgoal:

1 1. m :
2. k :
3. m = 0
( i:{k-m..k}. i+1) = 1
1 step

About:

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