IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc exteq gprop1211 1. A : Type
2. P : AProp
3. f : x:AProp(given P(x))
4. x : A 5. P(x)
6. f(x) Prop(given P(x))
f(x) Prop
By:
Rename5: w THEN Witness6: w
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
Prop(given P(x))
f(x) 
