A:Type, P:(AProp), B:(x:AType(given P(x))).
  x:{u:A| P(u) }B(x) =ext x:AB(x)(given P(x))

By:	SimilarTo Thm* B:(AProp), C:({u:A| B(u) }Type). Thm* x:{u:A| B(u) }C(x) =ext x:AC(x)(given B(x))

1

1. A : Type 2. P : AProp 3. B : x:AType(given P(x))   B  {u:A| P(u) }Type

1 step

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