A more intuitive proof that lists from a COFE

I tried to explain the old proof to @jihgfee, who wanted to prove that a more involved inductive data type is a COFE, and I failed badly. The current proof involves all kinds of magic involving seq and indexing on lists. As such, I decided to refactor the proof in a way that it became more understandable.

The current proof is actually documented, and should also scale to other inductive data types like trees (and hopefully @jihgfee's example).