Def  Msize(f) ==  i:k. f(i)

is mentioned by

Thm*  f:(a2).  Thm*  (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f)))	[card_st_vs_msize]
Def  size(a)(p) == Msize(x.if p(x) 1 else 0 fi)	[boolsize]
Def  a {k} T == {p:(aT)| Msize(p) = k }	[sized_mset]

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