Nuprl - Proof: swap cons 2 2 2 1

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

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, j)(i1))] = L[((i-1, j-1)(i1-1))]

By:	Subst' ((i, j)(i1) = (i-1, j-1)(i1-1)+1) 0 THEN Try (Complete (Unfold `flip` 0 THEN Reduce 0))

Generated subgoals:

1 (i, j)(i1) = (i-1, j-1)(i1-1)+1
1 step

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

About:

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

1	(i, j)(i1) = (i-1, j-1)(i1-1)+1	1 step
2	[x / L][((i-1, j-1)(i1-1)+1)] = L[((i-1, j-1)(i1-1))]	3 steps