Def  if b t else f fi == InjCase(b; . t, f)

is mentioned by

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)

[iter_via_intseg]

In prior sections: bool 1 LogicSupplement int 2 num thy 1

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