IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc pairing projs11 1. A : Type
2. B : AType
3. u : A 4. v : B(u)
<u,v> = <<u,v>.1,<u,v>.2> a:AB(a)
By:
Reduce Concl
Generated subgoal:
1
<u,v> = <u,v> a:AB(a)
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
<u,v> = <<u,v>.1,<u,v>.2> 
a:A
B(a)
