(6steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial tail via iter wf
  m,k:. k!m  
By: Def of k!m THEN UnivCD

Generated subgoal:

1 1. m : 
2. k : 
  ( i:{k-m..k}. i+1)  
5 steps

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

(6steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc