Theorem list.exists_of_mem_dmap

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

refactor(*): use 'lemma' iff statement is private

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