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