Type-checking naturally partial list functions can be rather onerous.
Therefore when possible I've made functions more total than they need to be.
Also, to simplify life for type checking I've made it so that all length restrictions are spun off as separate subgoals and avoided having multiple wf lemmas giving types both in List and List(n). IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html