Nuprl - Proof: proper sublist length 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: proper sublist length 1 1

1. T : Type
2. L1 : T List
3. L2 : T List
4. f :

||L1||

||L2||
5. increasing(f;||L1||)
6.

||L1||. L1[j] = L2[(f(j))]
7. ||L1|| = ||L2||
8. i :

9. i<||L1||
10. L1[i] = L2[(f(i))]

L1[i] = L2[i]

By:	Inst Thm* k:, f:(kk). increasing(f;k) (i:k. f(i) = i) [\|\|L1\|\|;f;i]

Generated subgoal:

1 11. f(i) = i
L1[i] = L2[i]
1 step

About:

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