diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 384e60c74b12ebcf86bc9cb9c6f32f39e451d2fa..4002d1d821aedea8544a46a4bf9a2b83ba274531 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -34,8 +34,9 @@ Section saved_prop.
Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ x y :
- saved_prop_own γ x ∗ saved_prop_own γ y ⊢ ▷ (x ≡ y).
+ saved_prop_own γ x -∗ saved_prop_own γ y -∗ ▷ (x ≡ y).
Proof.
+ apply wand_intro_r.
rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index f02b1078bff51a120d8077bf20b2afa5e3fa9a06..a216ff6ba0ebbda873b82161de87e86d7f5e5f9e 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -78,7 +78,7 @@ Proof.
iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
iDestruct (big_opS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
+ - iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_opS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
@@ -153,7 +153,7 @@ Proof.
iMod ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
{ iSplit; [iPureIntro; by eauto using wait_step|].
rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
+ iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
iModIntro. wp_if.
iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.