Ever closer to verifying monad laws for List.

There remain a couple of uses of  lemma-unsafe