IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
set functionality wrt one one corr n pred212 1. A : Type
2. B : AProp
3. B' : AProp
4. x:A. B(x) B'(x)
x:A. B(x) B'(Id(x))
By:
Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:A. B(x) 
B'(x)
