First series of results on lists.
List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)