Who Cites fun over st?
fun_over_st	Def  x:A st P(x)B(x) == x:{x:A| P(x) }B(x)

Syntax:

x:A st P(x)B(x)

has structure:

fun_over_st(A; x.P(x); x.B(x))

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html