Simplify soundness of the base logic.

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