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

is mentioned by

Thm* L:T List, P:(TT), n:(||L||-1). Thm* count(x < y in swap(L;n;n+1) | P(x,y)) Thm* = Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)] Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P,L[n]) Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if 1 Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+else 0 fi	[count_pairs_swap]
Def count(x < y in L | P(x;y)) Def == sum(if (i<j)P(L[i];L[j]) 1 else 0 fi | i < ||L||; j < ||L||)	[count_pairs]

In prior sections: bool 1 mb nat int 2 num thy 1 list 1 mb list 1

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