Trouble with iApply and typeclass inference order
The following says it all:
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.