IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hprod ty def131 1. 'a : S
2. 'b : S
3. x : 'a'bhbool
4. x' : hprod('a; 'b)
5. x = mk_pair(1of(x'),2of(x'))
x@0:'a, y:'b. x = mk_pair(x@0,y) 'a'b
By:
((DTerm 1of(x') 0) THEN (DTerm 2of(x') 0)) THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'b
x@0:'a, y:'b. x = mk_pair(x@0,y) 
'a
