IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fun description111 1. A : Type
2. B : AType
3. P : x:AB(x)Prop
4. x:A. y:B(x). y is the y:B(x). P(x,y)
5. f : x:AB(x)
6. x : A 7. f(x) is the y:B(x). P(x,y)
P(x,f(x))
By:
Analyze7
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
x:A. 
y:B(x). y is the y:B(x). P(x,y)
P(x,f(x))
