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

1	firstn(||v||+1;[u / (v @ l)]) ~ [u / firstn(||v||;v @ l)]	3 steps
2	[u / v] = [u / firstn(||v||;v @ l)]	1 step

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