diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v index 013a1e199f6b613301384c2716257d877ced6385..320355c44b423707d29249ccaa0dd52f2490c6b9 100644 --- a/tests/proofmode_monpred.v +++ b/tests/proofmode_monpred.v @@ -193,4 +193,12 @@ Section tests_iprop. iMod ("Hclose" with "H2"). iModIntro. iModIntro. by iNext. Qed. + + Lemma test_iPoseProof `{inG Σ A} P γ (x y : A) : + x ~~> y → P ∗ ⎡own γ x⎤ ==∗ ⎡own γ y⎤. + Proof. + iIntros (?) "[_ Hγ]". + iPoseProof (own_update with "Hγ") as "H"; first done. + by iMod "H". + Qed. End tests_iprop.