(35steps total) PrintForm Definitions int 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: comp nat ind tp 1
1. P : Prop
2. i:. (j:. j<i  P(j))  P(i)
  i:. P(i)
By: Analyze 0

Generated subgoal:

1 3. i : 
  P(i)
33 steps

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

(35steps total) PrintForm Definitions int 1 Sections StandardLIB Doc