IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ax choice111111 1. A : Type
2. B : Type
3. Q : ABProp
4. g : x:Ay:BQ(x,y)
5. x : A 6. y1 : B 7. y2 : Q(x,y1)
8. <y1,y2> = g(x)
Q(x,1of(<y1,y2>))
By:
AbReduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
B
Q(x,y)
Q(x,1of(<y1,y2>))
