Nuprl - Proof: swapped select 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swapped select 1 1

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

||L1||
5. j :

||L1||
6. L2 = swap(L1;i;j)
7. ||L2|| = ||L1||
8. L2 = swap(L1;i;j)

L1 = swap(swap(L1;i;j);i;j)

By:	RWO Thm* L1:T List, i,j:\|\|L1\|\|. swap(swap(L1;i;j);i;j) = L1 0

Generated subgoals:

None

About:

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