diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index a6793e3e54aa0af7d09b6e20ccbbf81954876c9a..4c93c721aea85fdce4f72c6f8c497148b54d1fa1 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,4 +1,4 @@
-Require Import prelude.gmap program_logic.lifting.
+Require Import prelude.gmap program_logic.lifting program_logic.ownership.
 Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
 Import uPred heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 509edcb65f4f12fee31d1e9af825ebc8d94f829c..6996b7096f7961dc5852513b46b3ace76505c6b3 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,5 +1,5 @@
 (** This file is essentially a bunch of testcases. *)
-Require Import program_logic.upred.
+Require Import program_logic.upred program_logic.ownership.
 Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang uPred notations.
 
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 9c0d6f3394cd5f7321fbee9b1efd1d9128e29769..930c17e496e014584ac2380082f6ef030c97bacc 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,5 +1,5 @@
 Require Export program_logic.hoare.
-Require Import program_logic.wsat.
+Require Import program_logic.wsat program_logic.ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/program_logic/global_cmra.v b/program_logic/global_cmra.v
index c93d2518c90e1af2bb7d72b52167f2ad51db21b0..a79fce247646ea05104d5a8ab017020899bb480d 100644
--- a/program_logic/global_cmra.v
+++ b/program_logic/global_cmra.v
@@ -1,24 +1,25 @@
-Require Export algebra.iprod program_logic.ownership program_logic.pviewshifts.
+Require Export algebra.iprod program_logic.pviewshifts.
+Require Import program_logic.ownership.
 Import uPred.
 
 Definition gid := positive.
-Definition globalC (Δ : gid → iFunctor) : iFunctor :=
-  iprodF (λ i, mapF gid (Δ i)).
+Definition globalC (Σ : gid → iFunctor) : iFunctor :=
+  iprodF (λ i, mapF gid (Σ i)).
 
-Class InG Λ (Δ : gid → iFunctor) (i : gid) (A : cmraT) :=
-  inG : A = Δ i (laterC (iPreProp Λ (globalC Δ))).
-Definition to_funC {Λ} {Δ : gid → iFunctor} (i : gid) 
-           `{!InG Λ Δ i A} (a : A) : Δ i (laterC (iPreProp Λ (globalC Δ))) :=
+Class InG Λ (Σ : gid → iFunctor) (i : gid) (A : cmraT) :=
+  inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))).
+Definition to_Σ {Λ} {Σ : gid → iFunctor} (i : gid) 
+           `{!InG Λ Σ i A} (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) :=
   eq_rect A id a _ inG.
-Definition to_globalC {Λ} {Δ : gid → iFunctor}
-           (i : gid) (γ : gid) `{!InG Λ Δ i A} (a : A) : iGst Λ (globalC Δ) :=
-  iprod_singleton i {[ γ ↦ to_funC _ a ]}.
-Definition own {Λ} {Δ : gid → iFunctor}
-    (i : gid) `{!InG Λ Δ i A} (γ : gid) (a : A) : iProp Λ (globalC Δ) :=
-  ownG (Σ:=globalC Δ) (to_globalC i γ a).
+Definition to_globalC {Λ} {Σ : gid → iFunctor}
+           (i : gid) (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) :=
+  iprod_singleton i {[ γ ↦ to_Σ _ a ]}.
+Definition own {Λ} {Σ : gid → iFunctor}
+    (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
+  ownG (to_globalC i γ a).
 
 Section global.
-Context {Λ : language} {Δ : gid → iFunctor} (i : gid) `{!InG Λ Δ i A}.
+Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}.
 Implicit Types a : A.
 
 (* Proeprties of to_globalC *)
@@ -27,7 +28,7 @@ Lemma globalC_op γ a1 a2 :
 Proof.
   rewrite /to_globalC iprod_op_singleton map_op_singleton.
   apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
-  by rewrite /to_funC; destruct inG.
+  by rewrite /to_Σ; destruct inG.
 Qed.
 
 Lemma globalC_validN n γ a :
@@ -35,7 +36,7 @@ Lemma globalC_validN n γ a :
 Proof.
   rewrite /to_globalC.
   rewrite -iprod_validN_singleton -map_validN_singleton.
-  by rewrite /to_funC; destruct inG.
+  by rewrite /to_Σ; destruct inG.
 Qed.
 
 (* Properties of own *)
@@ -43,7 +44,7 @@ Qed.
 Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
 Proof.
   intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
-  by rewrite /to_globalC /to_funC; destruct inG.
+  by rewrite /to_globalC /to_Σ; destruct inG.
 Qed.
 
 Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
@@ -54,14 +55,14 @@ Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
 (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc E a :
-  ✓a → True ⊑ pvs E E (∃ γ, own (Δ:=Δ) i γ a).
+  ✓a → True ⊑ pvs E E (∃ γ, own i γ a).
 Proof.
-  intros Hm. set (P m := ∃ γ, m = to_globalC (Δ:=Δ) i γ a).
+  intros Hm. set (P m := ∃ γ, m = to_globalC i γ a).
   rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
   - rewrite -pvs_updateP_empty //; [].
     subst P. eapply (iprod_singleton_updateP_empty i).
-    + eapply map_updateP_alloc' with (x:=to_funC i a).
-      by rewrite /to_funC; destruct inG.
+    + eapply map_updateP_alloc' with (x:=to_Σ i a).
+      by rewrite /to_Σ; destruct inG.
     + simpl. move=>? [γ [-> ?]]. exists γ. done.
   - apply exist_elim=>m. apply const_elim_l.
     move=>[p ->] {P}. by rewrite -(exist_intro p).
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 75cd71b80f0847fcadbb5baf72f67784e05e164d..b049cfb677aea41410a854b1c52063e593f53abc 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -1,4 +1,5 @@
 Require Export program_logic.hoare program_logic.lifting.
+Require Import program_logic.ownership.
 Import uPred.
 
 Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 295115aa92b1221e0a948170285dafb151ccb16e..98426ec3da588a7caf2ec4ae5df9663376b52269 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
 Require Export program_logic.weakestpre.
-Require Import program_logic.wsat.
+Require Import program_logic.wsat program_logic.ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/program_logic/namespace.v b/program_logic/namespace.v
index 76e8a34c09f3bd1884392ff625bc742ef393d4bc..2a98cc3ef63df1659abee0def542643932ce8fe2 100644
--- a/program_logic/namespace.v
+++ b/program_logic/namespace.v
@@ -1,5 +1,6 @@
 Require Export algebra.base prelude.countable prelude.co_pset.
-Require Export program_logic.ownership program_logic.pviewshifts.
+Require Import program_logic.ownership.
+Require Export program_logic.pviewshifts.
 
 Definition namespace := list positive.
 Definition nnil : namespace := nil.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index d9da27c12fac4d0c0082a27c7154db74877350e1..b9728d6430f54be40f9a0ab0a8abf7fccf8511d9 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,5 +1,6 @@
-Require Export program_logic.ownership prelude.co_pset.
-Require Import program_logic.wsat.
+Require Export prelude.co_pset.
+Require Export program_logic.model.
+Require Import program_logic.ownership program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 019fc6a1b7902f31e5dbfb045e2af3ce955edc11..812844f8730f132207009fb88e5e7f8de12543e4 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,4 +1,5 @@
 Require Export program_logic.pviewshifts.
+Require Import program_logic.ownership.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → pvs E1 E2 Q))%I.