B:(A
Type), p:(x:A
B(x)), C:Type, b:(x:AB(x)C).
Thm* (p/x,y. b(x,y)) = b(1of(p),2of(p))
B:(AType), p:(a:AB(a)). <1of(p),2of(p)> = p 
a:AB(a)A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))is mentioned by
| B:(AType), p:(x:AB(x)), C:Type, b:(x:AB(x)C).
Thm* (p/x,y. b(x,y)) = b(1of(p),2of(p)) | [spread_to_pi12] |
| B:(AType), p:(a:AB(a)). <1of(p),2of(p)> = p a:AB(a) | [pair_eta_rw] |
| A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) | [pi2_wf] |
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html