IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
all int segs by upper ind111 1. P : Prop
2. a:, b:{...a}. P(a,b)
3. a:, b:{a+1...}. (c:{a..b}. P(a,c)) P(a,b)
4. a : 5. b : {...a}
P(a,b)
By:
BackThru: Hyp:2
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
a:
}. P(a,c)) 
P(a,b)
P(a,b)
