deprecating List.nth in favor of List.nth_default

[andres-erbsen]

These definitions are equivalent on ground terms, and we should pick one to recommend so that lemmas consolidate around it unless there is a strong reason to keep both.