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)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] |
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html