Nuprl - Proof: firstn is iseg 1 1 1

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

1. T : Type
2. L1 : T List
3. l : T List

L1 = firstn(||L1||;L1 @ l)

By:	ListInd 2 THEN Reduce 0

Generated subgoals:

1 nil = firstn(0;l)
2 steps

2 4. u : T
5. v : T List
6. v = firstn(||v||;v @ l)
[u / v] = firstn(||v||+1;[u / (v @ l)])
5 steps

About:

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

1	nil = firstn(0;l)	2 steps
2	4. u : T 5. v : T List 6. v = firstn(\|\|v\|\|;v @ l) [u / v] = firstn(\|\|v\|\|+1;[u / (v @ l)])	5 steps