diff --git a/adequacy.v b/adequacy.v
index 113067d4522f9c79903a2351c31b75967550bd29..27f331573afc57d355f59766fb130126a44bff85 100644
--- a/adequacy.v
+++ b/adequacy.v
@@ -1,7 +1,6 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From lrust Require Export heap.
 From iris.algebra Require Import auth.
-From iris.program_logic Require Import ownership.
 From lrust Require Import proofmode notation.
 
 Class heapPreG Σ := HeapPreG {
diff --git a/heap.v b/heap.v
index 00f8240d72b2c55264e48816ccb776eed56443a1..cf583bec94eaf7aaf477f205726a4485f245d219 100644
--- a/heap.v
+++ b/heap.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import upred_big_op cmra_big_op gmap frac dec_agree.
 From iris.algebra Require Import csum excl auth.
-From iris.program_logic Require Export invariants ownership.
+From iris.program_logic Require Export invariants wsat.
 From iris.proofmode Require Export tactics.
 From lrust Require Export lifting.
 Import uPred.
@@ -468,8 +468,8 @@ Section heap.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
     iVs (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iApply pvs_intro'; [set_solver|iIntros "Hclose'"].
-    iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
+    iVs (pvs_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+    iVsIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
     iVs "Hclose'" as "_". iVs ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
     { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
     iVsIntro. clear dependent n σ hF.
@@ -519,8 +519,8 @@ Section heap.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
     iVs (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iApply pvs_intro'; [set_solver|iIntros "Hclose'"].
-    iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
+    iVs (pvs_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+    iVsIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
     iVs "Hclose'" as "_". iVs ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
     { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
     iVsIntro. clear dependent σ hF.
diff --git a/lifting.v b/lifting.v
index 8373138cec1f4de39ba9561e8e98bd1edc1a2237..e6d8d180fc56d8a8a8c46506b744e7b49186d5c6 100644
--- a/lifting.v
+++ b/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
+From iris.program_logic Require Import ectx_lifting wsat. (* for ownP *)
 From lrust Require Export lang.
 From lrust Require Import tactics.
 From iris.proofmode Require Import tactics.
diff --git a/races.v b/races.v
index 32cf4acd1cb12383a4bc9abfc4d3cf079ada5f44..c7273d30e8ce9a6749e72fb08c99926b1cc3ea51 100644
--- a/races.v
+++ b/races.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export hoare.
-From iris.program_logic Require Import ownership adequacy.
+From iris.program_logic Require Import adequacy.
 From lrust Require Import tactics.
 From iris.prelude Require Import gmap.