(4steps total) PrintForm NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc pairing projs

  A:Type, B:(AType), p:(u:AB(u)). p = <p.1,p.2>  a:AB(a)

By: UnivCD


Generated subgoal:

1 1. A : Type
2. B : AType
3. p : u:AB(u)
  p = <p.1,p.2>  a:AB(a)

3 steps

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

(4steps total) PrintForm NuprlPrimitives Sections NuprlLIB Doc