Nuprl - Proof: swap cons 2 2 2 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swap cons 2 2 2 1 2

1. T : Type
2. L : T List
3. x : T
4. i : {1..(||L||+1)

}
5. j : {1..(||L||+1)

}
6. i1 :

7. i1<||[x / L]||
8.

i1 = 0

[x / L][((i-1, j-1)(i1-1)+1)] = L[((i-1, j-1)(i1-1))]

By:	GenConcl ((i-1, j-1)(i1-1) = n) THENA Try (Complete Auto)

Generated subgoals:

1 (i-1, j-1)(i1-1) ||L||
1 step

2 9. n : ||L||
10. (i-1, j-1)(i1-1) = n
[x / L][(n+1)] = L[n]
1 step

About:

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

1	(i-1, j-1)(i1-1) \|\|L\|\|	1 step
2	9. n : \|\|L\|\| 10. (i-1, j-1)(i1-1) = n [x / L][(n+1)] = L[n]	1 step