IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exists over and r2 1. T : Type
2. A : Prop
3. B : TProp
4. A 5. x : T 6. B(x)
x:T. A & B(x)
By:
Witness x
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:T. A & B(x)
