Theorem list.forall_mem_cons_iff

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

refactor(*): attributes on same line

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