Nuprl - Proof: swap cons 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swap cons 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<||swap([x / L];i;j)||

swap([x / L];i;j)[i1] = [x / swap(L;i-1;j-1)][i1]

By:	CaseNat 0 `i1'

Generated subgoals:

1 8. i1 = 0
swap([x / L];i;j)[0] = [x / swap(L;i-1;j-1)][0]
4 steps

2 8. i1 = 0
swap([x / L];i;j)[i1] = [x / swap(L;i-1;j-1)][i1]
8 steps

About:

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

1	8. i1 = 0 swap([x / L];i;j)[0] = [x / swap(L;i-1;j-1)][0]	4 steps
2	8. i1 = 0 swap([x / L];i;j)[i1] = [x / swap(L;i-1;j-1)][i1]	8 steps