I would expect the following test to succeed:
Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M) : ▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q). Proof. iIntros "H". iNext. iAssumption. Qed.
