iNext does not strip off later below existential
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
Stripping off laters does happen below conjunctions, but not below existentials.