IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int seg upper ind1111 1. P : Prop
2. a : 3. b:{a...}. (c:{a..b}. P(a,c)) P(a,b)
4. k : 5. k1:. k1<k (b:{a...}. b-ak1P(a,b))
6. b : {a...}
7. b-ak 8. k = 0
P(a,b)
By:
BackThru: Hyp:3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html