Now that we have the plain modality, we can get rid of the basic updates
in the soundness statement.