Def  Iter(f;u) i:{a..b}. e(i)
Def  == if a<b f(Iter(f;u) i:{a..b-1}. e(i),e(b-1)) else u fi
Def  (recursive)

is mentioned by

Thm*  a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))	[card_sigma_vs_nsub_sigma]
Thm*  a,b,c:. c(ab) = (ca)b	[exp_exp_reduce2]
Thm*  a,b,c:. c(ab) = (cb)a	[exp_exp_reduce1]
Thm*  a,b:. (ab) ~ (ba)	[card_fun_vs_nsub_exp]
Thm*  a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))	[card_pi_vs_nsub_pi]
Def  Msize(f) ==  i:k. f(i)	[msize]

In prior sections: IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html