Theorem roption.exists_of_mem_bind

feat(computability/partrec): starting work on partial recursive funcs

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