Nuprl - Proof: int lt to int upper 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int lt to int upper 1

, A:({i+1...}

Prop). (

. i<j

A(j))

(

j:{i+1...}. A(j))

By:

GenUnivCD

Generated subgoals:

1 1. i :
2. A : {i+1...}Prop
3. j:. i<j  A(j)
4. j : {i+1...}
  A(j)
1 step

2 1. i :
2. A : {i+1...}Prop
3. j:{i+1...}. A(j)
4. j :
5. i<j
  A(j)
1 step

About:

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

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

1	1. i : 2. A : {i+1...}Prop 3. j:. i<j A(j) 4. j : {i+1...} A(j)	1 step
2	1. i : 2. A : {i+1...}Prop 3. j:{i+1...}. A(j) 4. j : 5. i<j A(j)	1 step