IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc exteq gfun1211 1. A : Type
2. B : AProp
3. C : {u:A| B(u) }Type
4. f : x:AC(x)(given B(x))
5. x : A 6. B(x)
7. f(x) C(x)(given B(x))
f(x) C(x)
By:
Witness-1: Hyp:6
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
C(x)(given B(x))
f(x) 
