Def  a {k}  == {p:(a)| size(a)(p) = k }

is mentioned by

Thm*  p:(a {k} ). {i:a| p(i) } ~ k	[card_st_sized_bool]
Thm*  (a {k} ) ~ (a {k} 2)	[card_boolset_vs_mset]

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