Implement the nodup function on lists and prove associated results.
Adds two lemmas about hderror to the List standard library.