IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
dep ax choice111111 1. A : Type
2. B : AType
3. Q : x:AB(x)Type
4. g : x:Ay:B(x)Q(x,y)
5. x : A 6. y1 : B(x)
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
Type
Q(x,y)
Q(x,1of(<y1,y2>))
