IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm*  a,b:e:({a..b}).
Thm*  a<b  ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))+e(b-1)
[sum_via_intseg_split_last]
cites the following:
1Thm*  f:(AAA), u:Aa,b:e:({a..b}A).
Thm*  a<b
Thm*  
Thm*  (Iter(f;ui:{a..b}. e(i)) = f((Iter(f;ui:{a..b-1}. e(i)),e(b-1))
[iter_via_intseg_split_last]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops Sections DiscrMathExt Doc