diff --git a/_CoqProject b/_CoqProject
index 6f18679ede63cf8188fd34628bd7404382ced25c..a38123baa312aace8c2df7fae0bf4aae302bd0d8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,7 +67,7 @@ program_logic/model.v
 program_logic/adequacy.v
 program_logic/lifting.v
 program_logic/invariants.v
-program_logic/ownership.v
+program_logic/wsat.v
 program_logic/weakestpre.v
 program_logic/pviewshifts.v
 program_logic/hoare.v
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 6da24be014129ca9e37e28552d830f3141b40363..c6e482cbad95c1aa8907dd784d98850beb855a0e 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.algebra Require Import auth.
-From iris.program_logic Require Import ownership auth.
+From iris.program_logic Require Import wsat auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 8f088062335c05e47702d85d1680f69b0fb6a57d..5701bd3136556c0a62aa504be5b125c6756ac29b 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth gmap frac dec_agree.
 From iris.program_logic Require Export invariants ghost_ownership.
-From iris.program_logic Require Import ownership auth.
+From iris.program_logic Require Import wsat auth.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 278165adb0f0d324b009188c8d92aa6ada6c45ee..917c0002535885440ee3463fcbb9b946834e9340 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/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 wsat ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 4b6540a71517af9c68ceca1c731d4a7bcbff075c..96377473f7932fa1bee8d1526db956ceac455b48 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index b43ead95ec2738b2795f44de64500150735a1ecd..7d329558b564a425bb82efff655babbb2abcf7d1 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -1,6 +1,6 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 
 Section wp.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 08b7407aeafa4ff9a41f59e2199bf451ec8b75bc..8fe284f2401764adb8f6a741f76ae90f8fe28e93 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Export namespaces.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index da791e981fcfdd125d79a3b104902ba5f7a45acc..b5f27323774c53dcee77174dd8fcf9f81f5172db 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Export upred_big_op.
 From iris.proofmode Require Import tactics.
 
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index cf2070e49ed4146c360b060e4bbed93cd1e375e3..2f6fb5c0a21a9b0d9d1c1dbd4b20f3b21fae50b0 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export iris.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import upred_big_op gmap.
 From iris.proofmode Require Import tactics classes.
 Import uPred.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9c8d93f85ad43402a71c975d9ec62f2bae3f6950..0e8244c0b6fc88865e3d0d3562330ef98592387a 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export pviewshifts.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics classes.
diff --git a/program_logic/ownership.v b/program_logic/wsat.v
similarity index 100%
rename from program_logic/ownership.v
rename to program_logic/wsat.v
diff --git a/tests/atomic.v b/tests/atomic.v
index 0b978bab802c84dd816be2935cbb01692c1d8457..72d20913d518166507a89e29b6b223e14a2b78c0 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
+From iris.program_logic Require Export hoare weakestpre pviewshifts.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics.
@@ -41,7 +41,9 @@ Section atomic.
   Arguments atomic_triple {_} _ _ _ _.
 End atomic.
 
+(* TODO: Importing in the middle of the file is bad practice. *)
 From iris.heap_lang Require Export lang proofmode notation.
+From iris.heap_lang.lib Require Import par.
 
 Section incr.
   Context `{!heapG Σ} (N : namespace).
@@ -92,7 +94,6 @@ Section incr.
   Qed.
 End incr.
 
-From iris.heap_lang.lib Require Import par.
 
 Section user.
   Context `{!heapG Σ, !spawnG Σ} (N : namespace).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 3a1a31fd2762dff8e943396b72faadb504082e62..bccc4848ca9410f450ead0a1f93a5427d0a2a7d6 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,7 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LiftingTests.