Def  x:A st P(x)B(x) == x:{x:A| P(x) }B(x)

is mentioned by

Thm*  (x:A. Dec(P(x))) Thm*   Thm*  ((x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x))))

[card_split_prod_intseg_family_decbl]

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