Tasks: - Make theorems such as `nextFD_numchars` into simps - Group simps such as `bumpFD_inode_tbl` and `bumpFD_files` into a single lemma - Prove other direction of lemmas such as `validFD_bumpFD` and add them into simps
Tasks:
nextFD_numcharsinto simpsbumpFD_inode_tblandbumpFD_filesinto a single lemmavalidFD_bumpFDand add them into simps