Def  a {k} T == {p:(aT)| Msize(p) = k }

is mentioned by

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