mb basic Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def l[i] == hd(nth_tl(i;l))

is mentioned by

Thm* x:Tl:T List, i:||l||. [x / l][(i+1)] ~ l[i][select_cons_tl_sq]

In prior sections: list 1

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb basic Sections MarkB generic Doc