Make clear which arguments of tactics are optional in `ProofMode.md`
See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050
See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050