diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v index e6e09aa41232ce6fdb36fc48ed75d4c8fdd08540..898e1e29964e0172fb7f624bf9c3a5bcd93618f8 100644 --- a/theories/lifetime/model/boxes.v +++ b/theories/lifetime/model/boxes.v @@ -235,7 +235,7 @@ Proof. iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ V) ∗ [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' None) ∗ box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]". - { rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]"). + { rewrite -big_sepM_sep -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]"). iAlways; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)". assert (Ho : from_option (⊑ V) False o) by eauto. destruct o as [V'|]=>//. rewrite -Ho.