IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
dep ax choice version211111 1. A : Type
2. B : AType
3. Q : x:AB(x)Prop
4. g : x:Ay:B(x)Q(x,y)
5. x : A 6. y : B(x)
7. w1 : Q(x,y)
8. <y,w1> = g(x)
Q(x,1of(<y,w1>))
By:
Compute 1of(<y,w1>) *y
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(<y,w1>))
y
