Nuprl - Proof: firstn is iseg 1 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn is iseg 1 1 1 2 1

1. T : Type
2. T List
3. l : T List
4. u : T
5. v : T List
6. v = firstn(||v||;v @ l)

firstn(||v||+1;[u / (v @ l)]) ~ [u / firstn(||v||;v @ l)]

By:	RW (AddrC [1] (RecUnfoldC `firstn`)) 0 THEN Reduce 0 THEN SplitOnConclITE

Generated subgoals:

1 7. 0<||v||+1
[u / firstn(||v||+1-1;v @ l)] ~ [u / firstn(||v||;v @ l)]
1 step

2 7. ||v||+10
nil ~ [u / firstn(||v||;v @ l)]
Auto

About:

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

1	7. 0<\|\|v\|\|+1 [u / firstn(\|\|v\|\|+1-1;v @ l)] ~ [u / firstn(\|\|v\|\|;v @ l)]	1 step
2	7. \|\|v\|\|+10 nil ~ [u / firstn(\|\|v\|\|;v @ l)]	Auto