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

is mentioned by

Thm* Y(f,x. if x=0 1 else xf(x-1) fi)	[sfa_doc_ycomb_factorial_typing]
Thm* (f,x. if x=0 1 else xf(x-1) fi)  (k:. (k)(k+1))	[sfa_doc_factbody_polytyping]
Thm* f,g:(). Thm* (x:. f zero beyond x) & (x:. g zero beyond x) Thm*  Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x)	[sfa_doc_alternate_zero_beyond]
Thm* f:().  Thm* (n:. f(n) = 0) Thm*  Thm* (n:. if f(n)=0 False else C:Prop{1}. C fi)  Prop{1}	[sfa_doc_predicativity_sample8]
Def i steps of e from a == if i=0 a else e(i-1 steps of e from a) fi Def (recursive)	[sfa_doc_sequence_rel]
Def max(a;b) == if a<b b else a fi	[sfa_doc_max_int]
Def A^n == if n=0 Unit ; n=1 A else A(A^(n-1)) fi  (recursive)	[sfa_doc_ntuple]
Def x! == if x=0 1 else x(x-2)! fi  (recursive)	[sfa_doc_factorial2]
Def x! == if x=0 1 else x(x-1)! fi  (recursive)	[sfa_doc_factorial]
Def mu(f) == if f(0) 0 else 1+mu(x.f(1+x)) fi  (recursive)	[kleene_minimize]

In prior sections: bool 1 int 2 list 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html