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

is mentioned by

Thm* x,y:A, P:(AProp), i,j:. Thm* P(if i=j x else y fi)  P(if i=j x else y fi)	[eq_int_cases_test]
Thm* f:(ST), b:, p,q:S. f(if b p else q fi) = if b f(p) else f(q) fi	[fun_thru_ite]
Thm* b:, x,y:T. b  if b x else y fi = x	[ite_rw_true]
Thm* b:, x,y:T. b  if b x else y fi = y	[ite_rw_false]
Def p  q == if p true else q fi	[bor]
Def pq == if p q else false fi	[band]
Def b == if b false else true fi	[bnot]
Def b2i(b) == if b 1 else 0 fi	[b2i]
Def b == if b True else False fi	[assert]

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