iNext does not strip off both laters from ▷ P ∗ ▷ Q
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.
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.