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

is mentioned by

Thm*  {x:A| if b P(x) else Q(x) fi } Thm*  =ext Thm*  if b {x:A| P(x) } else {x:A| Q(x) } fi	[ifthenelse_distr_subtype]
Def  AB == i:2. if i=0 A else B fi	[isect_two]

In prior sections: bool 1

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