Some minor uPred lemmas

Generalizes pure and later soundness to include ownM resources on the left-hand side, and adds a lemma for commuting later and bupd around plain propositions. The need for these arose when developing the NRL logic, which builds on top of Iris-Lean.