(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 1 2 1
1. P : Prop
2. i:. (j:. j<i  P(j))  P(i)
3. i : 
  i+1  
By: ArithMemberReflEqTypeCD

Generated subgoals:

1   i+1  
1 step
2   0i+1
3 steps
3 1. P : Prop{k}
2. i:. (j:. j<i  P(j))  P(i)
3. 
4. i1 : 
  (0i1)  Type{1}
1 step

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

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