slightly generalize and reorganize fupd soundness lemmas

Group the fupd and step_fupd soundness lemmas separately. Also make all these soundness lemmas work for arbitrary plain propositions. We seem to reflect this in the name as well, like fupd_plain, but do we really want to keep that naming convention? We will not have both versions of each lemma, so maybe we should just call them fupd_soundness and it is simply the case that those work for all plain P.

Furthermore tweak the uPred soundness statements so that they actually cover an arbitrary nesting of modalities.