Def list.product

feat(data/list): separate out list defs into `data.lists.defs`

feat(*): working on list/basic, robusting simp proofs

refactor(*): import content from lean/library/data and library_dev