Nuprl - Proof: select append front 1 2

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

1. T : Type
2. T List
3. bs : T List
4. u : T
5. v : T List
6.

||v||. (v @ bs)[i] = v[i]
7. i :

(||v||+1)

(u.(v @ bs))[i] = (u.v)[i]

By:	Decide (i = 0)

Generated subgoals:

1 8. i = 0
(u.(v @ bs))[i] = (u.v)[i]
1 step

2 8. i = 0
(u.(v @ bs))[i] = (u.v)[i]
2 steps

About:

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

1	8. i = 0 (u.(v @ bs))[i] = (u.v)[i]	1 step
2	8. i = 0 (u.(v @ bs))[i] = (u.v)[i]	2 steps