Def  size(a)(p) == Msize(x.if p(x) 1 else 0 fi)

is mentioned by

Thm*  p:(a). {x:a| p(x) } ~ (size(a)(p))	[card_st_vs_boolsize]
Def  a {k}  == {p:(a)| size(a)(p) = k }	[sized_bool]

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