Copyedit the proof mode documentation
As a side note, there's an (out-of-date) copy of ProofMode.md in FP/iris-tutorial; I'm not sure what your plans are for that repo, but I'd recommend removing ProofMode.md and pointing back to the Iris version so it stays up-to-date without maintenance.