(7steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int seg upper ind 1 1 1 2

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-ak1  P(a,b))
6. b : {a...}
7. b-ak
8. k = 0
  P(a,b)


By: BackThru: Hyp:3


Generated subgoal:

1 9. c : {a..b}
  P(a,c)

1 step

About:
intnatural_numbersubtractless_thanfunctionequalpropimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc