(6steps total) PrintForm Definitions Lemmas int 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: comp nat ind a 1
1. P : Prop
2. i:. (j:. j<i  P(j))  P(i)
3. i : 
  P(i)
By: Assert (j,s:. s<j  P(s))
THEN
IfLabL [`assertion`,Id;`main`,(InstHyp [i+1;i] -1)]

Generated subgoal:

1   j,s:. s<j  P(s)
4 steps

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

(6steps total) PrintForm Definitions Lemmas int 1 Sections StandardLIB Doc