Alternative definition of the basic update modality
This MR replaces the "double negation" file with the alternative definition of basic updates from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/186.
This MR replaces the "double negation" file with the alternative definition of basic updates from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/186.