diff --git a/CHANGELOG.md b/CHANGELOG.md
index fa2dfe45419b4239712e0dc2784eb391db44ce9f..b3463405bf38b76cc197a1123282cd6e995485f8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,8 +10,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   backwards compatibility and will be removed in a future version of Iris.
 * View shifts are radically simplified to just internalize frame-preserving
   updates.  Weakestpre is defined inside the logic, and invariants and view
-  shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
-  is proven in the logic.
+  shifts with masks are also coded up inside Iris.  Adequacy of weakestpre is
+  proven in the logic. [#] The old ownership of the entire physical state is
+  replaced by a user-selected predicate over physical state that is maintained
+  by weakestpre.
 * Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
   recursive domain equation.  As a consequence, CMRAs no longer need a proof
   of completeness.
diff --git a/_CoqProject b/_CoqProject
index de6d164eb9a6d7fad7020806efef78bc823f7891..11ce1cd1a4f03b813d8968eae9d3d50d1a7d93e9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -92,13 +92,13 @@ program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
+program_logic/gen_heap.v
+program_logic/ownp.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
-heap_lang/lifting.v
-heap_lang/derived.v
+heap_lang/rules.v
 heap_lang/notation.v
-heap_lang/heap.v
 heap_lang/lib/spawn.v
 heap_lang/lib/par.v
 heap_lang/lib/assert.v
diff --git a/algebra/auth.v b/algebra/auth.v
index d2311b0d59ff48cb5be48bfefffadc54bbce00c4..daa508e25748c0430c3de1279986979ead6441fd 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -275,7 +275,7 @@ Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
   (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
   constructor; simpl; auto.
-  apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
+  apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
 Qed.
 Instance auth_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 08117babe892f8415e2de5af006af85c64eb21a0..f75552747da6b23029bdb61df6bb70ab25d520f3 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1250,11 +1250,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply rFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
 Qed.
 
 Instance optionURF_contractive F :
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 0734d5c0f88198de0b1600607aec44a7286989f4..e6e4d23a8f2ac867cfd753fbe5b7deee608b3cb8 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -475,11 +475,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
 Qed.
 Instance gmapCF_contractive K `{Countable K} F :
   cFunctorContractive F → cFunctorContractive (gmapCF K F).
@@ -496,11 +496,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
 Qed.
 Instance gmapRF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
diff --git a/algebra/list.v b/algebra/list.v
index 5fd0616e8d8a5fe2b1d08665915a36b62d1c6ec6..9fca913634bc6c90bfb01f2dde0714c5c59b4d80 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -108,11 +108,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply cFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply cFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply cFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance listCF_contractive F :
@@ -452,11 +452,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply urFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply urFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
 Qed.
 
 Instance listURF_contractive F :
diff --git a/algebra/ofe.v b/algebra/ofe.v
index a24756ca26e81fc5d684b5dbf242f7cfbc39ad85..0e59c67278a40cf60c3b5b3cb321cca93b454e50 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -820,11 +820,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply cFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance optionCF_contractive F :
diff --git a/base_logic/lib/cancelable_invariants.v b/base_logic/lib/cancelable_invariants.v
index 0d4e9a3146785da55f1724ec255a487aab792d1b..468990508e39148a52f07b3b2fe0d4c2c306baa7 100644
--- a/base_logic/lib/cancelable_invariants.v
+++ b/base_logic/lib/cancelable_invariants.v
@@ -37,11 +37,14 @@ Section proofs.
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. done. Qed.
 
-  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ∗ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp.
-  Proof. rewrite /cinv_own -own_op own_valid. by iIntros "% !%". Qed.
+  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ✓ (q1 + q2)%Qp.
+  Proof. apply (own_valid_2 γ q1 q2). Qed.
 
-  Lemma cinv_own_1_l γ q : cinv_own γ 1 ∗ cinv_own γ q ⊢ False.
-  Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.
+  Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
+  Qed.
 
   Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
   Proof.
@@ -54,7 +57,7 @@ Section proofs.
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
     iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
-    iDestruct (cinv_own_1_l with "[$Hγ $Hγ']") as %[].
+    iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
   Qed.
 
   Lemma cinv_open E N γ p P :
@@ -62,8 +65,8 @@ Section proofs.
     cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv Hγ".
-    iInv N as "[$|>Hγ']" "Hclose".
+    iInv N as "[$ | >Hγ']" "Hclose".
     - iIntros "!> {$Hγ} HP". iApply "Hclose"; eauto.
-    - iDestruct (cinv_own_1_l with "[$Hγ $Hγ']") as %[].
+    - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
   Qed.
 End proofs.
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 1e33e4054ccc349e7887bdbd503629740cde1801..9c4d812ddd6b90e273ba1b34d3340828e051ae12 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,27 +1,26 @@
-From iris.program_logic Require Export weakestpre adequacy.
-From iris.heap_lang Require Export heap.
+From iris.program_logic Require Export weakestpre adequacy gen_heap.
+From iris.heap_lang Require Export rules.
 From iris.algebra Require Import auth.
-From iris.base_logic.lib Require Import wsat auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
 Class heapPreG Σ := HeapPreG {
-  heap_preG_iris :> irisPreG heap_lang Σ;
-  heap_preG_heap :> authG Σ heapUR
+  heap_preG_iris :> invPreG Σ;
+  heap_preG_heap :> gen_heapPreG loc val Σ
 }.
 
-Definition heapΣ : gFunctors :=
-  #[irisΣ state; authΣ heapUR].
+Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? ?]%subG_inv. split; apply _. Qed.
+Proof. intros [? ?]%subG_inv; split; apply _. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  (∀ `{heapG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
   adequate e σ φ.
 Proof.
-  intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iMod (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
-  { exact: to_heap_valid. }
-  set (Hheap := HeapG _ _ _ γ).
-  iApply (Hwp _). by rewrite /heap_ctx.
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
+  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
+  { apply: auth_auth_valid. exact: to_gen_heap_valid. }
+  iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
+  set (Hheap := GenHeapG loc val Σ _ _ _ _ γ).
+  iApply (Hwp (HeapG _ _ _)).
 Qed.
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
deleted file mode 100644
index 367f34eaaa077df0ceb77cb5b2d3e7b52297feac..0000000000000000000000000000000000000000
--- a/heap_lang/derived.v
+++ /dev/null
@@ -1,77 +0,0 @@
-From iris.heap_lang Require Export lifting.
-Import uPred.
-
-(** Define some derived forms, and derived lemmas about them. *)
-Notation Lam x e := (Rec BAnon x e).
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV x e := (RecV BAnon x e).
-Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
-
-Section derived.
-Context `{irisG heap_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-
-(** Proof rules for the sugar *)
-Lemma wp_lam E x elam e1 e2 Φ :
-  e1 = Lam x elam →
-  is_Some (to_val e2) →
-  Closed (x :b: []) elam →
-  ▷ WP subst' x e2 elam @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
-
-Lemma wp_let E x e1 e2 Φ :
-  is_Some (to_val e1) → Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
-Proof. by apply wp_lam. Qed.
-
-Lemma wp_seq E e1 e2 Φ :
-  is_Some (to_val e1) → Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. intros ??. by rewrite -wp_let. Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
-
-Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
-  ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
-
-Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
-  ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
-
-Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n2 < n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
-  P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
-Qed.
-
-Lemma wp_lt E (n1 n2 : Z) P Φ :
-  (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
-  P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
-Qed.
-
-Lemma wp_eq E e1 e2 v1 v2 P Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (v1 = v2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (v1 ≠ v2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
-  P ⊢ WP BinOp EqOp e1 e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (v1 = v2)); by eauto.
-Qed.
-End derived.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
deleted file mode 100644
index 923c7309a81b5c000afb6f12fbb34d888875aa4f..0000000000000000000000000000000000000000
--- a/heap_lang/heap.v
+++ /dev/null
@@ -1,194 +0,0 @@
-From iris.heap_lang Require Export lifting.
-From iris.algebra Require Import auth gmap frac dec_agree.
-From iris.base_logic.lib Require Export invariants.
-From iris.base_logic.lib Require Import wsat auth fractional.
-From iris.proofmode Require Import tactics.
-Import uPred.
-(* TODO: The entire construction could be generalized to arbitrary languages that have
-   a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
-   predicates over finmaps instead of just ownP. *)
-
-Definition heapN : namespace := nroot .@ "heap".
-Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
-
-(** The CMRA we need. *)
-Class heapG Σ := HeapG {
-  heapG_iris_inG :> irisG heap_lang Σ;
-  heap_inG :> authG Σ heapUR;
-  heap_name : gname
-}.
-
-Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
-
-Section definitions.
-  Context `{heapG Σ}.
-
-  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    auth_own heap_name ({[ l := (q, DecAgree v) ]}).
-  Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
-  Definition heap_mapsto := proj1_sig heap_mapsto_aux.
-  Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
-    proj2_sig heap_mapsto_aux.
-
-  Definition heap_ctx : iProp Σ := auth_ctx heap_name heapN to_heap ownP.
-End definitions.
-
-Typeclasses Opaque heap_ctx heap_mapsto.
-
-Notation "l ↦{ q } v" := (heap_mapsto l q v)
-  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
-Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
-
-Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
-  (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
-Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : uPred_scope.
-
-Section heap.
-  Context {Σ : gFunctors}.
-  Implicit Types P Q : iProp Σ.
-  Implicit Types Φ : val → iProp Σ.
-  Implicit Types σ : state.
-  Implicit Types h g : heapUR.
-
-  (** Conversion to heaps and back *)
-  Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
-  Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
-  Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
-  Lemma heap_singleton_included σ l q v :
-    {[l := (q, DecAgree v)]} ≼ to_heap σ → σ !! l = Some v.
-  Proof.
-    rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
-    move: Hl. rewrite /to_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
-    by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
-  Qed.
-  Lemma heap_singleton_included' σ l q v :
-    {[l := (q, DecAgree v)]} ≼ to_heap σ → to_heap σ !! l = Some (1%Qp,DecAgree v).
-  Proof.
-    intros Hl%heap_singleton_included. by rewrite /to_heap lookup_fmap Hl.
-  Qed.
-  Lemma to_heap_insert l v σ :
-    to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
-  Proof. by rewrite /to_heap fmap_insert. Qed.
-
-  Context `{heapG Σ}.
-
-  (** General properties of mapsto *)
-  Global Instance heap_ctx_persistent : PersistentP heap_ctx.
-  Proof. rewrite /heap_ctx. apply _. Qed.
-  Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
-  Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
-  Global Instance heap_mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
-  Proof.
-    unfold Fractional; intros.
-    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
-  Qed.
-  Global Instance heap_mapsto_as_fractional l q v :
-    AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-  Proof. done. Qed.
-
-  Lemma heap_mapsto_agree l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
-  Proof.
-    rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid
-            op_singleton singleton_valid.
-    f_equiv. move=>[_ ] /=.
-    destruct (decide (v1 = v2)) as [->|?]; first done. by rewrite dec_agree_ne.
-  Qed.
-
-  Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
-  Proof.
-    intros p q. iSplit.
-    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
-    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
-      iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->. iExists v2. by iFrame.
-  Qed.
-  Global Instance heap_ex_mapsto_as_fractional l q :
-    AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
-  Proof. done. Qed.
-
-  Lemma heap_mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
-  Proof.
-    rewrite heap_mapsto_eq /heap_mapsto_def auth_own_valid !discrete_valid.
-    by apply pure_mono=> /singleton_valid [??].
-  Qed.
-  Lemma heap_mapsto_valid_2 l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ✓ (q1 + q2)%Qp.
-  Proof.
-    iIntros "[H1 H2]". iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->.
-    iApply (heap_mapsto_valid l _ v2). by iFrame.
-  Qed.
-
-  (** Weakest precondition *)
-  Lemma wp_alloc E e v :
-    to_val e = Some v → ↑heapN ⊆ E →
-    {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
-  Proof.
-    iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
-    iMod (auth_empty heap_name) as "Ha".
-    iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_alloc_pst with "Hσ"). iNext. iIntros (l) "[% Hσ]".
-    iMod ("Hcl" with "* [Hσ]") as "Ha".
-    { iFrame. iPureIntro. rewrite to_heap_insert.
-      eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
-    iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
-  Qed.
-
-  Lemma wp_load E l q v :
-    ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E
-    {{{ RET v; l ↦{q} v }}}.
-  Proof.
-    iIntros (? Φ) "[#Hinv >Hl] HΦ".
-    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_load_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
-    iNext; iIntros "Hσ".
-    iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
-  Qed.
-
-  Lemma wp_store E l v' e v :
-    to_val e = Some v → ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E
-    {{{ RET LitV LitUnit; l ↦ v }}}.
-  Proof.
-    iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
-    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_store_pst _ σ with "Hσ"); first eauto using heap_singleton_included.
-    iNext; iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
-    { iFrame. iPureIntro. rewrite to_heap_insert.
-      eapply singleton_local_update, exclusive_local_update; last done.
-      by eapply heap_singleton_included'. }
-    by iApply "HΦ".
-  Qed.
-
-  Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
-    to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
-    {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
-  Proof.
-    iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ".
-    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_cas_fail_pst _ σ with "Hσ"); [eauto using heap_singleton_included|done|].
-    iNext; iIntros "Hσ".
-    iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
-  Qed.
-
-  Lemma wp_cas_suc E l e1 v1 e2 v2 :
-    to_val e1 = Some v1 → to_val e2 = Some v2 → ↑heapN ⊆ E →
-    {{{ heap_ctx ∗ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
-    {{{ RET LitV (LitBool true); l ↦ v2 }}}.
-  Proof.
-    iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
-    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
-    iApply (wp_cas_suc_pst _ σ with "Hσ"); first by eauto using heap_singleton_included.
-    iNext. iIntros "Hσ". iMod ("Hcl" with "* [Hσ]") as "Ha".
-    { iFrame. iPureIntro. rewrite to_heap_insert.
-      eapply singleton_local_update, exclusive_local_update; last done.
-      by eapply heap_singleton_included'. }
-    by iApply "HΦ".
-  Qed.
-End heap.
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 3ea46c969453c7ecd2a64007b343bc12e5b770d3..4ef9b4c8dd16d0bedcde67decc9551683eb8e275 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -402,3 +402,13 @@ Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
+
+(** Define some derived forms *)
+Notation Lam x e := (Rec BAnon x e).
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Notation Seq e1 e2 := (Let BAnon e1 e2).
+Notation LamV x e := (RecV BAnon x e).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
+Notation SeqCtx e2 := (LetCtx BAnon e2).
+Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index fa9b8cd257b635200a8e54644faecd74c775e0c5..511460f281cd053009262df410b36f115fd80b18 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -9,7 +9,7 @@ Definition assert : val :=
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
-  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
+  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
   iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 2b65b88c7d2d736a7d60b52d142c86e17e0acbdf..ee7d8d10c932c0c7d1d244b69707b2106be46208 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -38,7 +38,7 @@ Definition barrier_inv (l : loc) (P : iProp Σ) (s : state) : iProp Σ :=
   (l ↦ s ∗ ress (state_to_prop s P) (state_I s))%I.
 
 Definition barrier_ctx (γ : gname) (l : loc) (P : iProp Σ) : iProp Σ :=
-  (⌜heapN ⊥ N⌝ ∗ heap_ctx ∗ sts_ctx γ N (barrier_inv l P))%I.
+  sts_ctx γ N (barrier_inv l P).
 
 Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
   (∃ γ, barrier_ctx γ l P ∗ sts_ownS γ low_states {[ Send ]})%I.
@@ -73,11 +73,11 @@ Proof. solve_proper. Qed.
 (** Helper lemmas *)
 Lemma ress_split i i1 i2 Q R1 R2 P I :
   i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
-  saved_prop_own i Q ∗ saved_prop_own i1 R1 ∗ saved_prop_own i2 R2 ∗
-    (Q -∗ R1 ∗ R2) ∗ ress P I
-  ⊢ ress P ({[i1;i2]} ∪ I ∖ {[i]}).
+  saved_prop_own i Q -∗ saved_prop_own i1 R1 -∗ saved_prop_own i2 R2 -∗
+  (Q -∗ R1 ∗ R2) -∗ ress P I -∗
+  ress P ({[i1;i2]} ∪ I ∖ {[i]}).
 Proof.
-  iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
+  iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
   iDestruct (big_sepS_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.
@@ -91,10 +91,9 @@ Qed.
 
 (** Actual proofs *)
 Lemma newbarrier_spec (P : iProp Σ) :
-  heapN ⊥ N →
-  {{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
+  {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
 Proof.
-  iIntros (HN Φ) "#? HΦ".
+  iIntros (Φ) "HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with ">[-]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
@@ -120,7 +119,7 @@ Lemma signal_spec l P :
   {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}.
 Proof.
   rewrite /signal /send /barrier_ctx /=.
-  iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
+  iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_let.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   destruct p; [|done]. wp_store.
@@ -136,7 +135,7 @@ Lemma wait_spec l P:
   {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
-  iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
@@ -165,7 +164,7 @@ Lemma recv_split E l P1 P2 :
   ↑N ⊆ E → recv l (P1 ∗ P2) ={E}=∗ recv l P1 ∗ recv l P2.
 Proof.
   rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
-  iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   iMod (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".
@@ -176,7 +175,7 @@ Proof.
                    {[Change i1; Change i2 ]} with "[-]") as "Hγ".
   { iSplit; first by eauto using split_step.
     rewrite {2}/barrier_inv /=. iNext. iFrame "Hl".
-    iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
+    by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
   iAssert (sts_ownS γ (i_states i1) {[Change i1]}
     ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
@@ -191,8 +190,7 @@ Qed.
 
 Lemma recv_weaken l P1 P2 : (P1 -∗ P2) -∗ recv l P1 -∗ recv l P2.
 Proof.
-  rewrite /recv.
-  iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
+  rewrite /recv. iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
   iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
   iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
 Qed.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index 8df3af05138ba2b505d1484b70431046c4af3869..a733cb1e10e6a0806448e5278aac0068379d317d 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -8,19 +8,17 @@ Section spec.
 Context `{!heapG Σ} `{!barrierG Σ}.
 
 Lemma barrier_spec (N : namespace) :
-  heapN ⊥ N →
   ∃ recv send : loc → iProp Σ -n> iProp Σ,
-    (∀ P, heap_ctx ⊢ {{ True }} newbarrier #()
+    (∀ P, {{ True }} newbarrier #()
                      {{ v, ∃ l : loc, ⌜v = #l⌝ ∗ recv l P ∗ send l P }}) ∧
     (∀ l P, {{ send l P ∗ P }} signal #l {{ _, True }}) ∧
     (∀ l P, {{ recv l P }} wait #l {{ _, P }}) ∧
     (∀ l P Q, recv l (P ∗ Q) ={↑N}=> recv l P ∗ recv l Q) ∧
-    (∀ l P Q, (P -∗ Q) ⊢ recv l P -∗ recv l Q).
+    (∀ l P Q, (P -∗ Q) -∗ recv l P -∗ recv l Q).
 Proof.
-  intros HN.
   exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
   split_and?; simpl.
-  - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
+  - iIntros (P) "!# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
     iNext. eauto.
   - iIntros (l P) "!# [Hl HP]". iApply (signal_spec with "[$Hl $HP]"). by eauto.
   - iIntros (l P) "!# Hl". iApply (wait_spec with "Hl"). eauto.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 72d16f8300607cf998e00ff036993724af1cec15..45dcdf8aa0a6140200738b892d16c1201d715d0f 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export weakestpre.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac auth.
@@ -24,18 +25,16 @@ Section mono_proof.
     (∃ n, own γ (● (n : mnat)) ∗ l ↦ #n)%I.
 
   Definition mcounter (l : loc) (n : nat) : iProp Σ :=
-    (∃ γ, ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧
-          inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
+    (∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
 
   (** The main proofs. *)
   Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_mono_spec (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
+    {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
@@ -46,7 +45,7 @@ Section mono_proof.
     {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
-    iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
+    iDestruct "Hl" as (γ) "[#Hinv Hγf]".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
     iModIntro. wp_let. wp_op.
@@ -70,7 +69,7 @@ Section mono_proof.
   Lemma read_mono_spec l j :
     {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
   Proof.
-    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
+    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
       as %[?%mnat_included _]%auth_valid_discrete_2.
@@ -97,7 +96,7 @@ Section contrib_spec.
     (∃ n, own γ (● Some (1%Qp, n)) ∗ l ↦ #n)%I.
 
   Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
-    (⌜heapN ⊥ N⌝ ∧ heap_ctx ∧ inv N (ccounter_inv γ l))%I.
+    inv N (ccounter_inv γ l).
 
   Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
     own γ (◯ Some (q, n)).
@@ -108,11 +107,10 @@ Section contrib_spec.
   Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed.
 
   Lemma newcounter_contrib_spec (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx }}} newcounter #()
+    {{{ True }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+    iIntros (Φ) "HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (● (Some (1%Qp, O%nat)) ⋅ ◯ (Some (1%Qp, 0%nat))))
       as (γ) "[Hγ Hγ']"; first done.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
@@ -124,7 +122,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} incr #l
     {{{ RET #(); ccounter γ q (S n) }}}.
   Proof.
-    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ". iLöb as "IH". wp_rec.
+    iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
     iModIntro. wp_let. wp_op.
@@ -145,7 +143,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l
     {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
   Proof.
-    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
+    iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
       as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
@@ -157,7 +155,7 @@ Section contrib_spec.
     {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l
     {{{ n, RET #n; ccounter γ 1 n }}}.
   Proof.
-    iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
+    iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf") as %[Hn _]%auth_valid_discrete_2.
     apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index ffa2634c56c4379e241577a99f2ccc18fc233dfd..e9d37f8ab0fc405759253601fb9de74459e32bbc 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -1,4 +1,5 @@
-From iris.heap_lang Require Import heap notation.
+From iris.heap_lang Require Export rules notation.
+From iris.base_logic.lib Require Export invariants.
 
 Structure lock Σ `{!heapG Σ} := Lock {
   (* -- operations -- *)
@@ -14,11 +15,10 @@ Structure lock Σ `{!heapG Σ} := Lock {
   is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
   is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
   locked_timeless γ : TimelessP (locked γ);
-  locked_exclusive γ : locked γ ∗ locked γ ⊢ False;
+  locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (* -- operation specs -- *)
   newlock_spec N (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
   acquire_spec N γ lk R :
     {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}};
   release_spec N γ lk R :
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 3c15c0cd533eb5e4c627b3aa1ffcd1d4c4c6c75e..2fcad149b3ce6198c9a4fe01ff6ebabf7a296fd1 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -21,13 +21,13 @@ Context `{!heapG Σ, !spawnG Σ}.
    This is why these are not Texan triples. *)
 Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) :
   to_val e = Some (f1,f2)%V →
-  (heap_ctx ∗ WP f1 #() {{ Ψ1 }} ∗ WP f2 #() {{ Ψ2 }} ∗
-   ▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V)
-  ⊢ WP par e {{ Φ }}.
+  WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
+  (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
+  WP par e {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
+  iIntros (?) "Hf1 Hf2 HΦ".
   rewrite /par. wp_value. wp_let. wp_proj.
-  wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
+  wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
   wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
@@ -36,11 +36,11 @@ Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
     (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp Σ) :
-  (heap_ctx ∗ WP e1 {{ Ψ1 }} ∗ WP e2 {{ Ψ2 }} ∗
-   ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V)
-  ⊢ WP e1 ||| e2 {{ Φ }}.
+  WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
+  (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
+  WP e1 ||| e2 {{ Φ }}.
 Proof.
-  iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- $Hh $H]"); try wp_done.
-  iSplitL "H1"; by wp_let.
+  iIntros "H1 H2 H". iApply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); try wp_done.
+  by wp_let. by wp_let. auto.
 Qed.
 End proof.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 20cbb59b4246f6d43a6b99aa5451d934fbdf74f0..ab8d39d93b1a023cc6a94deae3cc75302c58dbd4 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export weakestpre.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
@@ -32,8 +33,7 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :
                    ∃ v, ⌜lv = SOMEV v⌝ ∗ (Ψ v ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
-  (⌜heapN ⊥ N⌝ ∗ ∃ γ, heap_ctx ∗ own γ (Excl ()) ∗
-                    inv N (spawn_inv γ l Ψ))%I.
+  (∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I.
 
 Typeclasses Opaque join_handle.
 
@@ -47,10 +47,9 @@ Proof. solve_proper. Qed.
 (** The main proofs. *)
 Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
   to_val e = Some f →
-  heapN ⊥ N →
-  {{{ heap_ctx ∗ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
+  {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
+  iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=.
   wp_let. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
@@ -65,7 +64,7 @@ Qed.
 Lemma join_spec (Ψ : val → iProp Σ) l :
   {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
 Proof.
-  rewrite /join_handle; iIntros (Φ) "[% H] HΦ". iDestruct "H" as (γ) "(#?&Hγ&#?)".
+  rewrite /join_handle; iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
   iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
@@ -73,7 +72,7 @@ Proof.
   - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
     + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
       iModIntro. wp_match. by iApply "HΦ".
-    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
+    + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
 Qed.
 End proof.
 
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index e9bcad0c6674cf9e939615a7a49124267b7a14ea..77a7dbbaa16d56830a44c18a39c57e053cbf79fb 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -26,12 +26,12 @@ Section proof.
     (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
 
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
-    (∃ l: loc, ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧ ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
+    (∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
 
   Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
 
-  Lemma locked_exclusive (γ : gname) : locked γ ∗ locked γ ⊢ False.
-  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
+  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
+  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
 
   Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
   Proof. solve_proper. Qed.
@@ -45,10 +45,9 @@ Section proof.
   Proof. apply _. Qed.
 
   Lemma newlock_spec (R : iProp Σ):
-    heapN ⊥ N →
-    {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
@@ -60,7 +59,7 @@ Section proof.
     {{{ is_lock γ lk R }}} try_acquire lk
     {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
   Proof.
-    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
+    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "[% #?]"; subst.
     wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
     - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
       iModIntro. iApply ("HΦ" $! false). done.
@@ -82,7 +81,7 @@ Section proof.
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
     iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
-    iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
+    iDestruct "Hlock" as (l) "[% #?]"; subst.
     rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
     wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
   Qed.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index e4c691e6bdf45e225bbb70d9300424ed55aa0253..477a28442946089bc8ba37292949537839283448 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -46,13 +46,11 @@ Section proof.
 
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     (∃ lo ln : loc,
-       ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧
-       ⌜lk = (#lo, #ln)%V⌝ ∧ inv N (lock_inv γ lo ln R))%I.
+       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R))%I.
 
   Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
     (∃ lo ln: loc,
-       ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧
-       ⌜lk = (#lo, #ln)%V⌝ ∧ inv N (lock_inv γ lo ln R) ∧
+       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R) ∗
        own γ (◯ (∅, GSet {[ x ]})))%I.
 
   Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, ∅)))%I.
@@ -67,17 +65,16 @@ Section proof.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
 
-  Lemma locked_exclusive (γ : gname) : (locked γ ∗ locked γ ⊢ False)%I.
+  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof.
-    iIntros "[H1 H2]". iDestruct "H1" as (o1) "H1". iDestruct "H2" as (o2) "H2".
-    iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _].
+    iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
+    iDestruct (own_valid_2 with "H1 H2") as %[[] _].
   Qed.
 
   Lemma newlock_spec (R : iProp Σ) :
-    heapN ⊥ N →
-    {{{ heap_ctx ∗ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock.
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
     iMod (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
@@ -90,7 +87,7 @@ Section proof.
   Lemma wait_loop_spec γ lk x R :
     {{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
   Proof.
-    iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
+    iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & Ht)".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
     iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -111,7 +108,7 @@ Section proof.
   Lemma acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
   Proof.
-    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
+    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "[% #?]".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
     iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
     wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
@@ -142,8 +139,7 @@ Section proof.
   Lemma release_spec γ lk R :
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
   Proof.
-    iIntros (Φ) "(Hl & Hγ & HR) HΦ".
-    iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
+    iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln) "[% #?]"; subst.
     iDestruct "Hγ" as (o) "Hγo".
     rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
deleted file mode 100644
index 8aef508f3a6e21be8aab5ffc41b36e34181c8fbd..0000000000000000000000000000000000000000
--- a/heap_lang/lifting.v
+++ /dev/null
@@ -1,183 +0,0 @@
-From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ectx_lifting.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import tactics.
-From iris.proofmode Require Import tactics.
-From iris.prelude Require Import fin_maps.
-Import uPred.
-
-(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
-[head_step]. The tactic will discharge head-reductions starting from values, and
-simplifies hypothesis related to conversions from and to values, and finite map
-operations. This tactic is slightly ad-hoc and tuned for proving our lifting
-lemmas. *)
-Ltac inv_head_step :=
-  repeat match goal with
-  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
-  | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | H : head_step ?e _ _ _ _ |- _ =>
-     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
-     and can thus better be avoided. *)
-     inversion H; subst; clear H
-  end.
-
-Local Hint Extern 0 (atomic _) => solve_atomic.
-Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
-
-Local Hint Constructors head_step.
-Local Hint Resolve alloc_fresh.
-Local Hint Resolve to_of_val.
-
-Section lifting.
-Context `{irisG heap_lang Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types efs : list expr.
-Implicit Types σ : state.
-
-(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
-Proof. exact: wp_ectx_bind. Qed.
-
-Lemma wp_bind_ctxi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
-     WP fill_item Ki e @ E {{ Φ }}.
-Proof. exact: weakestpre.wp_bind. Qed.
-
-(** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ v :
-  {{{ ▷ ownP σ }}} Alloc (of_val v) @ E
-  {{{ l, RET LitV (LitLoc l); ⌜σ !! l = None⌝ ∧ ownP (<[l:=v]>σ) }}}.
-Proof.
-  iIntros (Φ) "HP HΦ".
-  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
-  iSplitL; last by iApply big_sepL_nil. iApply "HΦ". by iSplit.
-Qed.
-
-Lemma wp_load_pst E σ l v :
-  σ !! l = Some v →
-  {{{ ▷ ownP σ }}} Load (Lit (LitLoc l)) @ E {{{ RET v; ownP σ }}}.
-Proof.
-  intros ? Φ. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_store_pst E σ l v v' :
-  σ !! l = Some v' →
-  {{{ ▷ ownP σ }}} Store (Lit (LitLoc l)) (of_val v) @ E
-  {{{ RET LitV LitUnit; ownP (<[l:=v]>σ) }}}.
-Proof.
-  intros. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_cas_fail_pst E σ l v1 v2 v' :
-  σ !! l = Some v' → v' ≠ v1 →
-  {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
-  {{{ RET LitV $ LitBool false; ownP σ }}}.
-Proof.
-  intros. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_cas_suc_pst E σ l v1 v2 :
-  σ !! l = Some v1 →
-  {{{ ▷ ownP σ }}} CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E
-  {{{ RET LitV $ LitBool true; ownP (<[l:=v2]>σ) }}}.
-Proof.
-  intros. apply wp_lift_atomic_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
-Proof.
-  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
-  - intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_rec E f x erec e1 e2 Φ :
-  e1 = Rec f x erec →
-  is_Some (to_val e2) →
-  Closed (f :b: x :b: []) erec →
-  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof.
-  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step' (App _ _)
-    (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_un_op E op e v v' Φ :
-  to_val e = Some v →
-  un_op_eval op v = Some v' →
-  ▷ Φ v' ⊢ WP UnOp op e @ E {{ Φ }}.
-Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
-    -?wp_value'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
-  bin_op_eval op v1 v2 = Some v' →
-  ▷ (Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
-    -?wp_value'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_if_true E e1 e2 Φ :
-  ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
-Proof.
-  apply wp_lift_pure_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_if_false E e1 e2 Φ :
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
-Proof.
-  apply wp_lift_pure_det_head_step'; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_fst E e1 v1 e2 Φ :
-  to_val e1 = Some v1 → is_Some (to_val e2) →
-  ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
-Proof.
-  intros ? [v2 ?].
-  rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_snd E e1 e2 v2 Φ :
-  is_Some (to_val e1) → to_val e2 = Some v2 →
-  ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
-Proof.
-  intros [v1 ?] ?.
-  rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value; eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_case_inl E e0 e1 e2 Φ :
-  is_Some (to_val e0) →
-  ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
-Proof.
-  intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e1 e0)); eauto.
-  intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_case_inr E e0 e1 e2 Φ :
-  is_Some (to_val e0) →
-  ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
-Proof.
-  intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e2 e0)); eauto.
-  intros; inv_head_step; eauto.
-Qed.
-End lifting.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index bd2bb6ff4cf2c9a3344136759983785d871f46ec..58ca9a1b29c43cd90117112ec909931ff3c80b47 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -1,5 +1,5 @@
-From iris.heap_lang Require Export derived.
-Export heap_lang.
+From iris.program_logic Require Import language.
+From iris.heap_lang Require Export lang tactics.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
@@ -91,15 +91,15 @@ Notation "e1 || e2" :=
   (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
-Notation NONE := (InjL #()).
-Notation SOME x := (InjR x).
+Notation NONE := (InjL #()) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
 
-Notation NONEV := (InjLV #()).
-Notation SOMEV x := (InjRV x).
+Notation NONEV := (InjLV #()) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
 
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
-  (e0, e1, x, e2 at level 200) : expr_scope.
+  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
 Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 309f2095bb27845de67368a79efd787755913fb8..08ae37f7937daff6827f3c9131907f60fb6bba34 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
-From iris.heap_lang Require Export wp_tactics heap.
+From iris.heap_lang Require Export wp_tactics rules.
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.
@@ -14,73 +14,63 @@ Implicit Types Δ : envs (iResUR Σ).
 
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
     (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
-  apply and_intro; first done.
-  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
+  intros ?? HΔ. eapply wand_apply; first exact: wp_alloc.
+  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
 
 Lemma tac_wp_load Δ Δ' E i l q v Φ :
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   to_val e = Some v' →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   (Δ'' ⊢ Φ (LitV LitUnit)) →
   Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
   (Δ' ⊢ Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   (Δ'' ⊢ Φ (LitV (LitBool true))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
-  apply and_intro; first done.
+  intros; subst. eapply wand_apply; first exact: wp_cas_suc.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -103,8 +93,6 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
     eapply tac_wp_alloc with _ H _;
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_alloc:" e' "not a value"
-      |iAssumption || fail "wp_alloc: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_alloc: cannot open heap invariant"
       |apply _
       |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
         eexists; split;
@@ -124,9 +112,7 @@ Tactic Notation "wp_load" :=
          match eval hnf in e' with Load _ => wp_bind_core K end)
       |fail 1 "wp_load: cannot find 'Load' in" e];
     eapply tac_wp_load;
-      [iAssumption || fail "wp_load: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_load: cannot open heap invariant"
-      |apply _
+      [apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
       |wp_finish]
@@ -143,8 +129,6 @@ Tactic Notation "wp_store" :=
     eapply tac_wp_store;
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_store:" e' "not a value"
-      |iAssumption || fail "wp_store: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_store: cannot open heap invariant"
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
@@ -165,8 +149,6 @@ Tactic Notation "wp_cas_fail" :=
        wp_done || fail "wp_cas_fail:" e' "not a value"
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_fail:" e' "not a value"
-      |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_cas_fail: cannot open heap invariant"
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -187,8 +169,6 @@ Tactic Notation "wp_cas_suc" :=
        wp_done || fail "wp_cas_suc:" e' "not a value"
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_suc:" e' "not a value"
-      |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
-      |solve_ndisj || fail "wp_cas_suc: cannot open heap invariant"
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
diff --git a/heap_lang/rules.v b/heap_lang/rules.v
new file mode 100644
index 0000000000000000000000000000000000000000..4aac38ac289fa824e069092a4077cfffa4300b1e
--- /dev/null
+++ b/heap_lang/rules.v
@@ -0,0 +1,276 @@
+From iris.program_logic Require Export weakestpre gen_heap.
+From iris.program_logic Require Import ectx_lifting.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import tactics.
+From iris.proofmode Require Import tactics.
+From iris.prelude Require Import fin_maps.
+Import uPred.
+
+Class heapG Σ := HeapG {
+  heapG_invG : invG Σ;
+  heapG_gen_heapG :> gen_heapG loc val Σ
+}.
+
+Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
+  iris_invG := heapG_invG;
+  state_interp := gen_heap_ctx
+}.
+
+(** Override the notations so that scopes and coercions work out *)
+Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
+Notation "l ↦ v" :=
+  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : uPred_scope.
+Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
+  (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
+Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : uPred_scope.
+
+(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
+[head_step]. The tactic will discharge head-reductions starting from values, and
+simplifies hypothesis related to conversions from and to values, and finite map
+operations. This tactic is slightly ad-hoc and tuned for proving our lifting
+lemmas. *)
+Ltac inv_head_step :=
+  repeat match goal with
+  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : _ = of_val ?v |- _ =>
+     is_var v; destruct v; first[discriminate H|injection H as H]
+  | H : head_step ?e _ _ _ _ |- _ =>
+     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
+     and can thus better be avoided. *)
+     inversion H; subst; clear H
+  end.
+
+Local Hint Extern 0 (atomic _) => solve_atomic.
+Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
+
+Local Hint Constructors head_step.
+Local Hint Resolve alloc_fresh.
+Local Hint Resolve to_of_val.
+
+Section rules.
+Context `{heapG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types efs : list expr.
+Implicit Types σ : state.
+
+(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
+Lemma wp_bind {E e} K Φ :
+  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Proof. exact: wp_ectx_bind. Qed.
+
+Lemma wp_bind_ctxi {E e} Ki Φ :
+  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ E {{ Φ }}.
+Proof. exact: weakestpre.wp_bind. Qed.
+
+(** Base axioms for core primitives of the language: Stateless reductions *)
+Lemma wp_fork E e Φ :
+  ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
+Proof.
+  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
+  - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
+  - intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_rec E f x erec e1 e2 Φ :
+  e1 = Rec f x erec →
+  is_Some (to_val e2) →
+  Closed (f :b: x :b: []) erec →
+  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
+Proof.
+  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
+    (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_un_op E op e v v' Φ :
+  to_val e = Some v →
+  un_op_eval op v = Some v' →
+  ▷ Φ v' ⊢ WP UnOp op e @ E {{ Φ }}.
+Proof.
+  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (UnOp op _) (of_val v'))
+    -?wp_value'; eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  bin_op_eval op v1 v2 = Some v' →
+  ▷ (Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
+Proof.
+  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val v'))
+    -?wp_value'; eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_if_true E e1 e2 Φ :
+  ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
+Proof.
+  apply wp_lift_pure_det_head_step_no_fork; eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_if_false E e1 e2 Φ :
+  ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
+Proof.
+  apply wp_lift_pure_det_head_step_no_fork; eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_fst E e1 v1 e2 Φ :
+  to_val e1 = Some v1 → is_Some (to_val e2) →
+  ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
+Proof.
+  intros ? [v2 ?].
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1) -?wp_value; eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_snd E e1 e2 v2 Φ :
+  is_Some (to_val e1) → to_val e2 = Some v2 →
+  ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
+Proof.
+  intros [v1 ?] ?.
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2) -?wp_value; eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_case_inl E e0 e1 e2 Φ :
+  is_Some (to_val e0) →
+  ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
+Proof.
+  intros [v0 ?].
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e1 e0)); eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+Lemma wp_case_inr E e0 e1 e2 Φ :
+  is_Some (to_val e0) →
+  ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
+Proof.
+  intros [v0 ?].
+  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e2 e0)); eauto.
+  intros; inv_head_step; eauto.
+Qed.
+
+(** Heap *)
+Lemma wp_alloc E e v :
+  to_val e = Some v →
+  {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+Proof.
+  iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>"; iSplit; first by auto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_load E l q v :
+  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l ↦{q} v }}}.
+Proof.
+  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_store E l v' e v :
+  to_val e = Some v →
+  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}.
+Proof.
+  iIntros (<-%of_to_val Φ) ">Hl HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
+  to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
+  {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+  {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
+Proof.
+  iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_suc E l e1 v1 e2 v2 :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+  {{{ RET LitV (LitBool true); l ↦ v2 }}}.
+Proof.
+  iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
+
+(** Proof rules for derived constructs *)
+Lemma wp_lam E x elam e1 e2 Φ :
+  e1 = Lam x elam →
+  is_Some (to_val e2) →
+  Closed (x :b: []) elam →
+  ▷ WP subst' x e2 elam @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
+
+Lemma wp_let E x e1 e2 Φ :
+  is_Some (to_val e1) → Closed (x :b: []) e2 →
+  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
+Proof. by apply wp_lam. Qed.
+
+Lemma wp_seq E e1 e2 Φ :
+  is_Some (to_val e1) → Closed [] e2 →
+  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
+Proof. intros ??. by rewrite -wp_let. Qed.
+
+Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
+Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
+
+Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
+  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
+  ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
+
+Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
+  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
+  ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
+
+Lemma wp_le E (n1 n2 : Z) P Φ :
+  (n1 ≤ n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (n2 < n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
+Qed.
+
+Lemma wp_lt E (n1 n2 : Z) P Φ :
+  (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
+Qed.
+
+Lemma wp_eq E e1 e2 v1 v2 P Φ :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  (v1 = v2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+  (v1 ≠ v2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  P ⊢ WP BinOp EqOp e1 e2 @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (v1 = v2)); by eauto.
+Qed.
+End rules.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 65fff20b5bbeec940954bcb3045ac84071b5f477..85c1e30b98ca8103da0c0045a08cca5c4dde4ed3 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Export tactics derived.
+From iris.heap_lang Require Export tactics rules.
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 91b8aebb7605bf7c7cd580b36109dcadf04a06e9..34006bcb608d7b546712c6cb9a794ea30c9ea681 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -556,7 +556,7 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
 Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
   g ∘ f <$> m = g <$> f <$> m.
 Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
-Lemma map_fmap_setoid_ext `{Equiv A, Equiv B} (f1 f2 : A → B) m :
+Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) m :
   (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <$> m ≡ f2 <$> m.
 Proof.
   intros Hi i; rewrite !lookup_fmap.
diff --git a/prelude/list.v b/prelude/list.v
index 72cd5c6a9b108e3a76b60a13eeaadf4e7ad0e36b..dbd6e73b72a1712d6021d8eb075357c890bc3239 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -2802,7 +2802,7 @@ Section fmap.
   Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
     (∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
   Proof. intros ? <-. induction l1; f_equal/=; auto. Qed.
-  Lemma list_fmap_setoid_ext `{Equiv B} (g : A → B) l :
+  Lemma list_fmap_equiv_ext `{Equiv B} (g : A → B) l :
     (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
   Proof. induction l; constructor; auto. Qed.
 
diff --git a/prelude/option.v b/prelude/option.v
index 24544dabf150910ff59137c184c79e6d889084ee..66fe22107bdffb6c5baad967423adf6b7c036299 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -180,7 +180,7 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed.
 Lemma fmap_Some {A B} (f : A → B) mx y :
   f <$> mx = Some y ↔ ∃ x, mx = Some x ∧ y = f x.
 Proof. destruct mx; naive_solver. Qed.
-Lemma fmap_Some_setoid {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
+Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
       (f : A → B) mx y :
   f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
 Proof.
@@ -190,6 +190,10 @@ Proof.
   - intros ?%symmetry%equiv_None. done.
   - intros (? & ? & ?). done.
 Qed.
+Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
+      (f : A → B) mx y :
+  f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x.
+Proof. by rewrite fmap_Some_equiv. Qed.
 Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None.
 Proof. by destruct mx. Qed.
 Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
@@ -200,7 +204,7 @@ Proof. by destruct mx. Qed.
 Lemma option_fmap_ext {A B} (f g : A → B) mx :
   (∀ x, f x = g x) → f <$> mx = g <$> mx.
 Proof. intros; destruct mx; f_equal/=; auto. Qed.
-Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A → B) mx :
+Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) mx :
   (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
 Proof. destruct mx; constructor; auto. Qed.
 Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 1ebdb806436da3f08ac6d773201490acd153b65a..43a0b12e03cc31d76c2217977f6b79dfdff28a89 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -22,21 +22,6 @@ Proof.
   intros [?%subG_inG [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv; by constructor.
 Qed.
 
-
-Definition irisΣ (Λstate : Type) : gFunctors :=
-  #[invΣ;
-    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].
-
-Class irisPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
-  inv_inG :> invPreG Σ;
-  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
-}.
-Notation irisPreG Λ Σ := (irisPreG' (state Λ) Σ).
-
-Instance subG_irisΣ {Λstate Σ} : subG (irisΣ Λstate) Σ → irisPreG' Λstate Σ.
-Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
-
-
 (* Allocation *)
 Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
@@ -49,17 +34,6 @@ Proof.
   iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
 Qed.
 
-Lemma iris_alloc `{irisPreG' Λstate Σ} σ :
-  (|==> ∃ _ : irisG' Λstate Σ, wsat ∗ ownE ⊤ ∗ ownP_auth σ ∗ ownP σ)%I.
-Proof.
-  iIntros.
-  iMod wsat_alloc as (?) "[Hws HE]".
-  iMod (own_alloc (● (Excl' (σ:leibnizC Λstate)) ⋅ ◯ (Excl' σ)))
-    as (γσ) "[Hσ Hσ']"; first done.
-  iModIntro; iExists (IrisG _ _ _ _ γσ). rewrite /ownP_auth /ownP; iFrame.
-Qed.
-
-
 (* Program logic adequacy *)
 Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
@@ -91,7 +65,7 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation world σ := (wsat ∗ ownE ⊤ ∗ ownP_auth σ)%I.
+Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
 
 Notation wptp t := ([∗ list] ef ∈ t, WP ef {{ _, True }})%I.
 
@@ -104,8 +78,7 @@ Proof.
   rewrite fupd_eq /fupd_def.
   iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
   iModIntro; iNext.
-  iMod ("H" $! e2 σ2 efs with "[%] [Hw HE]")
-    as ">($ & $ & $ & $)"; try iFrame; eauto.
+  by iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)".
 Qed.
 
 Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
@@ -178,50 +151,57 @@ Proof.
   iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
-Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ :
+Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  (I ={⊤,∅}=∗ ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
-  I ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ σ2⌝.
+  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
+  ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ⌝.
 Proof.
-  intros ? HI. rewrite wptp_steps //.
-  rewrite (Nat_iter_S_r (S n)) bupd_iter_frame_l. apply bupd_iter_mono.
-  iIntros "[HI H]".
+  intros ?. rewrite wptp_steps //.
+  rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l. apply bupd_iter_mono.
+  iIntros "[Hback H]".
   iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
-  rewrite fupd_eq in HI;
-    iMod (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
-  iDestruct "H" as (σ2') "[Hσf %]".
-  iDestruct (ownP_agree σ2 σ2' with "[-]") as %<-. by iFrame. eauto.
+  rewrite fupd_eq.
+  iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
 Qed.
 End adequacy.
 
-Theorem wp_adequacy Σ `{irisPreG Λ Σ} e σ φ :
-  (∀ `{irisG Λ Σ}, ownP σ ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
+  (∀ `{Hinv : invG Σ},
+     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }}) →
   adequate e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
     eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-    rewrite Nat_iter_S. iMod (iris_alloc σ) as (?) "(?&?&?&Hσ)".
-    iModIntro. iNext. iApply wptp_result; eauto.
-    iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
+    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iDestruct "Hwp" as (Istate) "[HI Hwp]".
+    iModIntro. iNext. iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto.
+    iFrame. by iApply big_sepL_nil.
   - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-    rewrite Nat_iter_S. iMod (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
-    iModIntro. iNext. iApply wptp_safe; eauto.
-    iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
+    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iDestruct "Hwp" as (Istate) "[HI Hwp]".
+    iModIntro. iNext. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto.
+    iFrame. by iApply big_sepL_nil.
 Qed.
 
-Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
-  (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=∗ I ∗ WP e {{ Φ }}) →
-  (∀ `{irisG Λ Σ}, I ={⊤,∅}=∗ ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ Φ :
+  (∀ `{Hinv : invG Σ},
+     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ1 ∗ WP e {{ Φ }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝)) →
   rtc step ([e], σ1) (t2, σ2) →
-  φ σ2.
+  φ.
 Proof.
-  intros Hwp HI [n ?]%rtc_nsteps.
+  intros Hwp [n ?]%rtc_nsteps.
   eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-  rewrite Nat_iter_S. iMod (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
-  rewrite fupd_eq in Hwp.
-  iMod (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
-  iModIntro. iNext. iApply wptp_invariance; eauto. iFrame. by iApply big_sepL_nil.
+  rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+  rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+  iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
+  iModIntro. iNext. iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto.
+  iFrame "Hw HE Hwp HIstate Hclose". by iApply big_sepL_nil.
 Qed.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 7341fd48e0813f26ed13f4a042b5dff293ebad58..2011826e699d3f8602855b0d9949c9fb52b3f6e7 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -16,15 +16,17 @@ Lemma wp_ectx_bind {E e} K Φ :
 Proof. apply: weakestpre.wp_bind. Qed.
 
 Lemma wp_lift_head_step E Φ e1 :
-  (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
-    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-          ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros "H". iApply (wp_lift_step E); try done.
-  iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
-  iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
-  iApply ("Hwp" with "* []"); by eauto.
+  iIntros (?) "H". iApply (wp_lift_step E)=>//. iIntros (σ1) "Hσ".
+  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
+  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H". by eauto.
 Qed.
 
 Lemma wp_lift_pure_head_step E Φ e1 :
@@ -38,47 +40,48 @@ Proof.
   iIntros (????). iApply "H". eauto.
 Qed.
 
-Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
-  head_reducible e1 σ1 →
-  ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
-  ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-    default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+Lemma wp_lift_atomic_head_step {E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      state_interp σ2 ∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
-  iIntros (???) "% ?". iApply ("H" with "* []"); eauto.
+  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
 Qed.
 
-Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
-  head_reducible e1 σ1 →
-  (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
-    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-  ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
-    Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
   ⊢ WP e1 @ E {{ Φ }}.
-Proof. eauto using wp_lift_atomic_det_step. Qed.
-
-Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 :
-  head_reducible e1 σ1 →
-  (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
-    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-  {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
-  rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
+  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iNext; iIntros (v2 σ2 efs) "%".
+  iMod ("H" $! v2 σ2 efs with "[#]") as "(% & $ & $)"=>//; subst.
+  by iApply big_sepL_nil.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  (∀ σ1 e2' σ2 efs',
+    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_pure_det_step. Qed.
 
-Lemma wp_lift_pure_det_head_step' {E Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+  (∀ σ1 e2' σ2 efs',
+    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
diff --git a/program_logic/gen_heap.v b/program_logic/gen_heap.v
new file mode 100644
index 0000000000000000000000000000000000000000..1d80623a6a0ae258edd1a81552dfa3a3a35c812b
--- /dev/null
+++ b/program_logic/gen_heap.v
@@ -0,0 +1,145 @@
+From iris.algebra Require Import auth gmap frac dec_agree.
+From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
+Import uPred.
+
+Definition gen_heapUR (L V : Type) `{Countable L, EqDecision V} : ucmraT :=
+  gmapUR L (prodR fracR (dec_agreeR V)).
+Definition to_gen_heap `{Countable L, EqDecision V} : gmap L V → gen_heapUR L V :=
+  fmap (λ v, (1%Qp, DecAgree v)).
+
+(** The CMRA we need. *)
+Class gen_heapG (L V : Type) (Σ : gFunctors)
+    `{Countable L, EqDecision V} := GenHeapG {
+  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
+  gen_heap_name : gname
+}.
+
+Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L, EqDecision V} :=
+  { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
+
+Definition gen_heapΣ (L V : Type) `{Countable L, EqDecision V} : gFunctors :=
+  #[GFunctor (constRF (authR (gen_heapUR L V)))].
+
+Instance subG_gen_heapPreG {Σ} `{Countable L, EqDecision V} :
+  subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
+Proof. intros ?%subG_inG; split; apply _. Qed.
+
+Section definitions.
+  Context `{gen_heapG L V Σ}.
+
+  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
+    own gen_heap_name (● to_gen_heap σ).
+
+  Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
+    own gen_heap_name (â—¯ {[ l := (q, DecAgree v) ]}).
+  Definition mapsto_aux : { x | x = @mapsto_def }. by eexists. Qed.
+  Definition mapsto := proj1_sig mapsto_aux.
+  Definition mapsto_eq : @mapsto = @mapsto_def := proj2_sig mapsto_aux.
+End definitions.
+
+Local Notation "l ↦{ q } v" := (mapsto l q v)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
+Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : uPred_scope.
+
+Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
+  (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
+Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : uPred_scope.
+
+Section gen_heap.
+  Context `{gen_heapG L V Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : V → iProp Σ.
+  Implicit Types σ : gmap L V.
+  Implicit Types h g : gen_heapUR L V.
+
+  (** Conversion to heaps and back *)
+  Lemma to_gen_heap_valid σ : ✓ to_gen_heap σ.
+  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
+  Lemma lookup_to_gen_heap_None σ l : σ !! l = None → to_gen_heap σ !! l = None.
+  Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
+  Lemma gen_heap_singleton_included σ l q v :
+    {[l := (q, DecAgree v)]} ≼ to_gen_heap σ → σ !! l = Some v.
+  Proof.
+    rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
+    move: Hl. rewrite /to_gen_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
+    by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
+  Qed.
+  Lemma to_gen_heap_insert l v σ :
+    to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_gen_heap σ).
+  Proof. by rewrite /to_gen_heap fmap_insert. Qed.
+
+  (** General properties of mapsto *)
+  Global Instance mapsto_timeless l q v : TimelessP (l ↦{q} v).
+  Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
+  Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
+  Proof.
+    intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
+      op_singleton pair_op dec_agree_idemp.
+  Qed.
+  Global Instance mapsto_as_fractional l q v :
+    AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
+  Proof. done. Qed.
+
+  Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
+  Proof.
+    rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
+    by move=> [_ /= /dec_agree_op_inv [?]].
+  Qed.
+
+  Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
+  Proof.
+    intros p q. iSplit.
+    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
+    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
+      iDestruct (mapsto_agree with "[$H1 $H2]") as %->. iExists v2. by iFrame.
+  Qed.
+  Global Instance heap_ex_mapsto_as_fractional l q :
+    AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
+  Proof. done. Qed.
+
+  Lemma mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
+  Proof.
+    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
+    by apply pure_mono=> /auth_own_valid /singleton_valid [??].
+  Qed.
+  Lemma mapsto_valid_2 l q1 q2 v1 v2 :
+    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ✓ (q1 + q2)%Qp.
+  Proof.
+    iIntros "[H1 H2]". iDestruct (mapsto_agree with "[$H1 $H2]") as %->.
+    iApply (mapsto_valid l _ v2). by iFrame.
+  Qed.
+
+  Lemma gen_heap_alloc σ l v :
+    σ !! l = None → gen_heap_ctx σ ==∗ gen_heap_ctx (<[l:=v]>σ) ∗ l ↦ v.
+  Proof.
+    iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iMod (own_update with "Hσ") as "[Hσ Hl]".
+    { eapply auth_update_alloc,
+        (alloc_singleton_local_update _ _ (1%Qp, DecAgree v))=> //.
+      by apply lookup_to_gen_heap_None. }
+    iModIntro. rewrite to_gen_heap_insert. iFrame.
+  Qed.
+
+  Lemma gen_heap_valid σ l q v : gen_heap_ctx σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
+  Proof.
+    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iDestruct (own_valid_2 with "Hσ Hl")
+      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2; auto.
+  Qed.
+
+  Lemma gen_heap_update σ l v1 v2 :
+    gen_heap_ctx σ -∗ l ↦ v1 ==∗ gen_heap_ctx (<[l:=v2]>σ) ∗ l ↦ v2.
+  Proof.
+    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iDestruct (own_valid_2 with "Hσ Hl")
+      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
+    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
+    { eapply auth_update, singleton_local_update,
+        (exclusive_local_update _ (1%Qp, DecAgree v2))=> //.
+      by rewrite /to_gen_heap lookup_fmap Hl. }
+    iModIntro. rewrite to_gen_heap_insert. iFrame.
+  Qed.
+End gen_heap.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index ea95a1c7a675fd6b6c0e7701ad457b749bcbe6f1..21b48a27aa2a00d4bf01212bda7b049d190a6aa9 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -11,23 +11,15 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
 Lemma wp_lift_step E Φ e1 :
-  (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
-    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-          ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof.
-  iIntros "H". rewrite wp_unfold /wp_pre.
-  destruct (to_val e1) as [v|] eqn:EQe1.
-  - iLeft. iExists v. iSplit. done. iMod "H" as (σ1) "[% _]".
-    by erewrite reducible_not_val in EQe1.
-  - iRight; iSplit; eauto.
-    iIntros (σ1) "Hσ". iMod "H" as (σ1') "(% & >Hσf & H)".
-    iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
-    iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
-    iMod (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
-    iApply ("H" with "* []"); eauto.
-Qed.
+Proof. iIntros (?) "H". rewrite wp_unfold /wp_pre; auto. Qed.
 
+(** Derived lifting lemmas. *)
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
@@ -35,41 +27,30 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
     WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
-  { iPureIntro. eapply reducible_not_val, (Hsafe inhabitant). }
+  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
+  { eapply reducible_not_val, (Hsafe inhabitant). }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
   iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
   iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
 Qed.
 
-(** Derived lifting lemmas. *)
-Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
-  reducible e1 σ1 →
-  (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-    default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+Lemma wp_lift_atomic_step {E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      state_interp σ2 ∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "[Hσ H]". iApply (wp_lift_step E _ e1).
-  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
-  iExists σ1. iFrame "Hσ"; iSplit; eauto.
-  iNext; iIntros (e2 σ2 efs) "% Hσ".
-  iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
+  iIntros (?) "H". iApply (wp_lift_step E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
+  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+  iModIntro; iNext; iIntros (e2 σ2 efs) "%". iMod "Hclose" as "_".
+  iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
   destruct (to_val e2) eqn:?; last by iExFalso.
-  iMod "Hclose". iApply wp_value; auto using to_of_val. done.
-Qed.
-
-Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
-  reducible e1 σ1 →
-  (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
-                   σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-  ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
-    Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
-Proof.
-  iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
-  iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
-  edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
+  by iApply wp_value.
 Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
diff --git a/program_logic/ownp.v b/program_logic/ownp.v
new file mode 100644
index 0000000000000000000000000000000000000000..14add9b238178c661544a0f6ddf07b07be6cba47
--- /dev/null
+++ b/program_logic/ownp.v
@@ -0,0 +1,231 @@
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import lifting adequacy.
+From iris.program_logic Require ectx_language.
+From iris.algebra Require Import auth.
+From iris.proofmode Require Import tactics classes.
+
+Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
+  ownP_invG : invG Σ;
+  ownP_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
+  ownP_name : gname;
+}.
+Notation ownPG Λ Σ := (ownPG' (state Λ) Σ).
+
+Instance ownPG_irisG `{ownPG' Λstate Σ} : irisG' Λstate Σ := {
+  iris_invG := ownP_invG;
+  state_interp σ := own ownP_name (● (Excl' (σ:leibnizC Λstate)))
+}.
+
+Definition ownPΣ (Λstate : Type) : gFunctors :=
+  #[invΣ;
+    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].
+
+Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
+  ownPPre_invG :> invPreG Σ;
+  ownPPre_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
+}.
+Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
+
+Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ → ownPPreG' Λstate Σ.
+Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
+
+
+(** Ownership *)
+Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
+  own ownP_name (◯ (Excl' σ)).
+Typeclasses Opaque ownP.
+Instance: Params (@ownP) 3.
+
+
+(* Adequacy *)
+Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} e σ φ :
+  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  adequate e σ φ.
+Proof.
+  intros Hwp. apply (wp_adequacy Σ _).
+  iIntros (?) "". iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
+    as (γσ) "[Hσ Hσf]"; first done.
+  iModIntro. iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
+  iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
+Qed.
+
+Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ Φ :
+  (∀ `{ownPG Λ Σ},
+    ownP σ1 ={⊤}=∗ WP e {{ Φ }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+  rtc step ([e], σ1) (t2, σ2) →
+  φ σ2.
+Proof.
+  intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _ Φ)=> //.
+  iIntros (?) "". iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
+    as (γσ) "[Hσ Hσf]"; first done.
+  iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
+  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
+  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
+  iDestruct (own_valid_2 with "Hσ Hσf")
+    as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
+Qed.
+
+
+(** Lifting *)
+Section lifting.
+  Context `{ownPG Λ Σ}.
+  Implicit Types e : expr Λ.
+  Implicit Types Φ : val Λ → iProp Σ.
+
+  Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
+  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
+  Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
+  Proof. rewrite /ownP; apply _. Qed.
+
+  Lemma ownP_lift_step E Φ e1 :
+    (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
+      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
+            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
+    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
+      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
+      move: Hred; by rewrite to_of_val.
+    - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
+      iMod "H" as (σ1') "(% & >Hσf & H)". rewrite /ownP.
+      iDestruct (own_valid_2 with "Hσ Hσf")
+        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+      iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
+      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
+      { by apply auth_update, option_local_update,
+          (exclusive_local_update _ (Excl σ2)). }
+      iFrame "Hσ". iApply ("H" with "* []"); eauto.
+  Qed.
+
+  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
+    (∀ σ1, reducible e1 σ1) →
+    (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
+    (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
+      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
+    { eapply reducible_not_val, (Hsafe inhabitant). }
+    iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+    iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+    destruct (Hstep σ1 e2 σ2 efs); auto; subst.
+    iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
+  Qed.
+
+  (** Derived lifting lemmas. *)
+  Lemma ownP_lift_atomic_step {E Φ} e1 σ1 :
+    reducible e1 σ1 →
+    (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (?) "[Hσ H]". iApply (ownP_lift_step E _ e1).
+    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
+    iExists σ1. iFrame "Hσ"; iSplit; eauto.
+    iNext; iIntros (e2 σ2 efs) "% Hσ".
+    iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
+    destruct (to_val e2) eqn:?; last by iExFalso.
+    iMod "Hclose". iApply wp_value; auto using to_of_val. done.
+  Qed.
+
+  Lemma ownP_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
+    reducible e1 σ1 →
+    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+                     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
+    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
+      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (ownP_lift_atomic_step _ σ1); try done.
+    iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
+    edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
+  Qed.
+
+  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
+    (∀ σ1, reducible e1 σ1) →
+    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (? Hpuredet) "?". iApply (ownP_lift_pure_step E); try done.
+    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
+  Qed.
+End lifting.
+
+Section ectx_lifting.
+  Import ectx_language.
+  Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
+  Context `{ownPG (ectx_lang expr) Σ} `{Inhabited state}.
+  Implicit Types Φ : val → iProp Σ.
+  Implicit Types e : expr.
+  Hint Resolve head_prim_reducible head_reducible_prim_step.
+
+  Lemma ownP_lift_head_step E Φ e1 :
+    (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
+      ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
+            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros "H". iApply (ownP_lift_step E); try done.
+    iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
+    iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
+    iApply ("Hwp" with "* []"); by eauto.
+  Qed.
+
+  Lemma ownP_lift_pure_head_step E Φ e1 :
+    (∀ σ1, head_reducible e1 σ1) →
+    (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
+    (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
+      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
+    iIntros (????). iApply "H". eauto.
+  Qed.
+
+  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
+    head_reducible e1 σ1 →
+    ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
+    ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iFrame. iNext.
+    iIntros (???) "% ?". iApply ("H" with "* []"); eauto.
+  Qed.
+
+  Lemma ownP_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
+    head_reducible e1 σ1 →
+    (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
+      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
+    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof. eauto using ownP_lift_atomic_det_step. Qed.
+
+  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
+    head_reducible e1 σ1 →
+    (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
+      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
+    {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
+  Proof.
+    intros. rewrite -(ownP_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
+    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
+  Qed.
+
+  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
+    (∀ σ1, head_reducible e1 σ1) →
+    (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
+  Proof. eauto using wp_lift_pure_det_step. Qed.
+
+  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
+    to_val e1 = None →
+    (∀ σ1, head_reducible e1 σ1) →
+    (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+  Proof.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+  Qed.
+End ectx_lifting.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 5cf0ae79372b04a5819f03a78c8102d12faa7f33..31d3d48dcfb20ec961339618b76dc948e341d25a 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -2,26 +2,14 @@ From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-From iris.algebra Require Import auth.
 Import uPred.
 
-Class irisG' (Λstate : Type) (Σ : gFunctors) : Set := IrisG {
+Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
-  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
-  state_name : gname;
+  state_interp : Λstate → iProp Σ;
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-Definition ownP `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
-  own state_name (◯ (Excl' σ)).
-Typeclasses Opaque ownP.
-Instance: Params (@ownP) 3.
-
-Definition ownP_auth `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
-  own state_name (● (Excl' (σ:leibnizC Λstate))).
-Typeclasses Opaque ownP_auth.
-Instance: Params (@ownP_auth) 4.
-
 Definition wp_pre `{irisG Λ Σ}
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ, (
@@ -29,9 +17,9 @@ Definition wp_pre `{irisG Λ Σ}
   (∃ v, ⌜to_val e1 = Some v⌝ ∧ |={E}=> Φ v) ∨
   (* step case *)
   (⌜to_val e1 = None⌝ ∧ ∀ σ1,
-     ownP_auth σ1 ={E,∅}=∗ ⌜reducible e1 σ1⌝ ∗
+     state_interp σ1 ={E,∅}=∗ ⌜reducible e1 σ1⌝ ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-       ownP_auth σ2 ∗ wp E e2 Φ ∗
+       state_interp σ2 ∗ wp E e2 Φ ∗
        [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)))%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
@@ -109,23 +97,6 @@ Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
-(* Physical state *)
-Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
-Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
-Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
-Proof. rewrite /ownP; apply _. Qed.
-
-Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ∗ ownP σ2 ⊢ ⌜σ1 = σ2⌝.
-Proof.
-  rewrite /ownP /ownP_auth -own_op own_valid -auth_both_op.
-  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
-Qed.
-Lemma ownP_update σ1 σ2 : ownP_auth σ1 ∗ ownP σ1 ==∗ ownP_auth σ2 ∗ ownP σ2.
-Proof.
-  rewrite /ownP -!own_op.
-  by apply own_update, auth_update, option_local_update, exclusive_local_update.
-Qed.
-
 (* Weakest pre *)
 Lemma wp_unfold E e Φ : WP e @ E {{ Φ }} ⊣⊢ wp_pre wp E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index d9f173c180f0dabcb15ac7e8dc3bc0b0cc091cbd..d27cddd6a1241f5f463ee5b580f5eb840e537cc2 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -18,39 +18,38 @@ Section client.
   Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
     (∃ f : val, l ↦{q} f ∗ □ ∀ n : Z, WP f #n {{ v, ⌜v = #(n + 42)⌝ }})%I.
 
-  Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ∗ y_inv (q/2) l).
+  Lemma y_inv_split q l : y_inv q l -∗ (y_inv (q/2) l ∗ y_inv (q/2) l).
   Proof.
     iDestruct 1 as (f) "[[Hl1 Hl2] #Hf]".
     iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
   Qed.
 
   Lemma worker_safe q (n : Z) (b y : loc) :
-    heap_ctx ∗ recv N b (y_inv q y) ⊢ WP worker n #b #y {{ _, True }}.
+    recv N b (y_inv q y) -∗ WP worker n #b #y {{ _, True }}.
   Proof.
-    iIntros "[#Hh Hrecv]". wp_lam. wp_let.
-    wp_apply (wait_spec with "[- $Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]".
+    iIntros "Hrecv". wp_lam. wp_let.
+    wp_apply (wait_spec with "Hrecv"). iDestruct 1 as (f) "[Hy #Hf]".
     wp_seq. wp_load.
     iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
   Qed.
 
-  Lemma client_safe : heapN ⊥ N → heap_ctx ⊢ WP client {{ _, True }}.
+  Lemma client_safe : WP client {{ _, True }}%I.
   Proof.
-    iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
-    wp_apply (newbarrier_spec N (y_inv 1 y) with "Hh"); first done.
+    iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
+    wp_apply (newbarrier_spec N (y_inv 1 y)).
     iIntros (l) "[Hr Hs]". wp_let.
-    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[-$Hh]"). iSplitL "Hy Hs".
+    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
     - (* The original thread, the sender. *)
       wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
       iSplitR "Hy"; first by eauto.
       iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
-      iSplitL; [|by iIntros (_ _) "_ !>"].
       iDestruct (recv_weaken with "[] Hr") as "Hr".
       { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
       iMod (recv_split with "Hr") as "[H1 H2]"; first done.
-      iApply (wp_par (λ _, True%I) (λ _, True%I) with "[- $Hh]").
-      iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ !>"]];
-        iApply worker_safe; by iSplit.
+      iApply (wp_par (λ _, True%I) (λ _, True%I) with "[H1] [H2]"); last auto.
+      + by iApply worker_safe.
+      + by iApply worker_safe.
 Qed.
 End client.
 
@@ -60,8 +59,7 @@ Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
 
 Lemma client_adequate σ : adequate client σ (λ _, True).
 Proof.
-  apply (heap_adequacy Σ)=> ?.
-  apply (client_safe (nroot .@ "barrier")); auto with ndisj.
+  apply (heap_adequacy Σ)=> ?. apply (client_safe (nroot .@ "barrier")).
 Qed.
 
 End ClosedProofs.
diff --git a/tests/counter.v b/tests/counter.v
index a97e466e26e575398b00388fe2e1231692878290..291ed8f1460c5546b63135098e5d3c1262f84ebd 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -84,19 +84,19 @@ Definition I (γ : gname) (l : loc) : iProp Σ :=
   (∃ c : nat, l ↦ #c ∗ own γ (Auth c))%I.
 
 Definition C (l : loc) (n : nat) : iProp Σ :=
-  (∃ N γ, ⌜heapN ⊥ N⌝ ∧ heap_ctx ∧ inv N (I γ l) ∧ own γ (Frag n))%I.
+  (∃ N γ, inv N (I γ l) ∧ own γ (Frag n))%I.
 
 (** The main proofs. *)
 Global Instance C_persistent l n : PersistentP (C l n).
 Proof. apply _. Qed.
 
-Lemma newcounter_spec N :
-  heapN ⊥ N →
-  heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
+Lemma newcounter_spec :
+  {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
 Proof.
-  iIntros (?) "#Hh !# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
+  iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
   iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
   rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
+  set (N := nroot .@ "C").
   iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
   { iIntros "!>". iExists 0%nat. by iFrame. }
   iModIntro. rewrite /C; eauto 10.
@@ -106,16 +106,17 @@ Lemma incr_spec l n :
   {{ C l n }} incr #l {{ v, ⌜v = #()⌝ ∧ C l (S n) }}.
 Proof.
   iIntros "!# Hl /=". iLöb as "IH". wp_rec.
-  iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
+  iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
   wp_bind (! _)%E; iInv N as (c) "[Hl Hγ]" "Hclose".
   wp_load. iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
   iModIntro. wp_let. wp_op.
   wp_bind (CAS _ _ _). iInv N as (c') ">[Hl Hγ]" "Hclose".
   destruct (decide (c' = c)) as [->|].
-  - iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
-    iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
-    rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
+  - iDestruct (own_valid_2 with "Hγ Hγf") as %?%auth_frag_valid.
+    iMod (own_update_2 with "Hγ Hγf") as "Hγ".
+    { rewrite -auth_frag_op. apply M_update. done. }
+    rewrite (auth_frag_op (S n) (S c)); last omega.
+    iDestruct "Hγ" as "[Hγ Hγf]".
     wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]").
     { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
     iModIntro. wp_if. rewrite {3}/C; eauto 10.
@@ -127,7 +128,7 @@ Qed.
 Lemma read_spec l n :
   {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
 Proof.
-  iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
+  iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
   rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
   iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
   { iApply own_op. by iFrame. }
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 60160c224cbf04d9404d613d54ea3e13b5d7efbc..8e3c473c7cb22e0f4f8ec159d9703d44a1a973e2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -11,10 +11,10 @@ Section LiftingTests.
 
   Definition heap_e  : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
-  Lemma heap_e_spec E :
-    ↑heapN ⊆ E → heap_ctx ⊢ WP heap_e @ E {{ v, ⌜v = #2⌝ }}.
+
+  Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
   Proof.
-    iIntros (HN) "#?". rewrite /heap_e.
+    iIntros "". rewrite /heap_e.
     wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
   Qed.
 
@@ -22,10 +22,10 @@ Section LiftingTests.
     let: "x" := ref #1 in
     let: "y" := ref #1 in
     "x" <- !"x" + #1 ;; !"x".
-  Lemma heap_e2_spec E :
-    ↑heapN ⊆ E → heap_ctx ⊢ WP heap_e2 @ E {{ v, ⌜v = #2⌝ }}.
+
+  Lemma heap_e2_spec E : WP heap_e2 @ E {{ v, ⌜v = #2⌝ }}%I.
   Proof.
-    iIntros (HN) "#?". rewrite /heap_e2.
+    iIntros "". rewrite /heap_e2.
     wp_alloc l. wp_let. wp_alloc l'. wp_let.
     wp_load. wp_op. wp_store. wp_load. done.
   Qed.
@@ -40,7 +40,7 @@ Section LiftingTests.
 
   Lemma FindPred_spec n1 n2 E Φ :
     n1 < n2 →
-    Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
+    Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
     iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
     wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
@@ -48,7 +48,7 @@ Section LiftingTests.
     - by assert (n1 = n2 - 1) as -> by omega.
   Qed.
 
-  Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.
+  Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) -∗ WP Pred #n @ E {{ Φ }}.
   Proof.
     iIntros "HΦ". wp_lam. wp_op=> ?; wp_if.
     - wp_op. wp_op.
@@ -62,5 +62,5 @@ Section LiftingTests.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
-Lemma heap_e_adequate σ : adequate heap_e σ (λ v, v = #2).
+Lemma heap_e_adequate σ : adequate heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 2a143a107b42abb8241c6e9ef4ba234a04057767..ecf84402c7ea78f1c3f478f1e207165b88995893 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -31,29 +31,28 @@ Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ :=
   (∃ x, own γ (Shot x) ∗ Φ x)%I.
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
-  recv N l (barrier_res γ Φ) ∗ (∀ x, {{ Φ x }} e {{ _, Ψ x }})
-  ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
+  recv N l (barrier_res γ Φ) -∗ (∀ x, {{ Φ x }} e {{ _, Ψ x }}) -∗
+  WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
-  iIntros "[Hl #He]". wp_apply (wait_spec with "[- $Hl]"); simpl.
+  iIntros "Hl #He". wp_apply (wait_spec with "[- $Hl]"); simpl.
   iDestruct 1 as (x) "[#Hγ Hx]".
   wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|].
   iIntros (v) "?"; iExists x; by iSplit.
 Qed.
 
 Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp Σ).
-Context {Φ_split : ∀ x, Φ x ⊢ (Φ1 x ∗ Φ2 x)}.
-Context {Ψ_join  : ∀ x, (Ψ1 x ∗ Ψ2 x) ⊢ Ψ x}.
+Context {Φ_split : ∀ x, Φ x -∗ (Φ1 x ∗ Φ2 x)}.
+Context {Ψ_join  : ∀ x, Ψ1 x -∗ Ψ2 x -∗ Ψ x}.
 
-Lemma P_res_split γ : barrier_res γ Φ ⊢ barrier_res γ Φ1 ∗ barrier_res γ Φ2.
+Lemma P_res_split γ : barrier_res γ Φ -∗ barrier_res γ Φ1 ∗ barrier_res γ Φ2.
 Proof.
   iDestruct 1 as (x) "[#Hγ Hx]".
   iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
 Qed.
 
-Lemma Q_res_join γ : barrier_res γ Ψ1 ∗ barrier_res γ Ψ2 ⊢ ▷ barrier_res γ Ψ.
+Lemma Q_res_join γ : barrier_res γ Ψ1 -∗ barrier_res γ Ψ2 -∗ ▷ barrier_res γ Ψ.
 Proof.
-  iIntros "[Hγ Hγ']";
-  iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']".
+  iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']".
   iAssert (▷ (x ≡ x'))%I as "Hxx".
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=.
@@ -62,24 +61,22 @@ Proof.
     { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
     rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
   iNext. iRewrite -"Hxx" in "Hx'".
-  iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
+  iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
 Qed.
 
 Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
-  heapN ⊥ N →
-  heap_ctx ∗ P
-  ∗ {{ P }} eM {{ _, ∃ x, Φ x }}
-  ∗ (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
-  ∗ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }})
-  ⊢ WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
+  P -∗
+  {{ P }} eM {{ _, ∃ x, Φ x }} -∗
+  (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -∗
+  (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -∗
+  WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
-  iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
+  iIntros "/= HP #He #He1 #He2"; rewrite /client.
   iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
-  wp_apply (newbarrier_spec N (barrier_res γ Φ) with "Hh"); auto.
+  wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
   iIntros (l) "[Hr Hs]".
   set (workers_post (v : val) := (barrier_res γ Ψ1 ∗ barrier_res γ Ψ2)%I).
-  wp_let. wp_apply (wp_par  (λ _, True)%I workers_post with "[- $Hh]").
-  iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
+  wp_let. wp_apply (wp_par  (λ _, True)%I workers_post with "[HP Hs Hγ] [Hr]").
   - wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|].
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
     iMod (own_update with "Hγ") as "Hx".
@@ -89,11 +86,10 @@ Proof.
   - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
     iMod (recv_split with "Hr") as "[H1 H2]"; first done.
     wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
-                     (λ _, barrier_res γ Ψ2)%I with "[-$Hh]").
-    iSplitL "H1"; [|iSplitL "H2"].
-    + iApply worker_spec; auto.
-    + iApply worker_spec; auto.
+                     (λ _, barrier_res γ Ψ2)%I with "[H1] [H2]").
+    + iApply (worker_spec with "H1"); auto.
+    + iApply (worker_spec with "H2"); auto.
     + auto.
-  - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
+  - iIntros (_ v) "[_ [H1 H2]]". iDestruct (Q_res_join with "H1 H2") as "?". auto.
 Qed.
 End proof.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 10cc5bf35b46470162ce0ac0734aa1f89c46f7e0..77846047e054131907e71de989ed2cac47e9a3e7 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -26,11 +26,11 @@ Definition rev : val :=
     end.
 
 Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp Σ) :
-  heap_ctx ∗ is_list hd xs ∗ is_list acc ys ∗
-    (∀ w, is_list w (reverse xs ++ ys) -∗ Φ w)
-  ⊢ WP rev hd acc {{ Φ }}.
+  is_list hd xs -∗ is_list acc ys -∗
+    (∀ w, is_list w (reverse xs ++ ys) -∗ Φ w) -∗
+  WP rev hd acc {{ Φ }}.
 Proof.
-  iIntros "(#Hh & Hxs & Hys & HΦ)".
+  iIntros "Hxs Hys HΦ".
   iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
   destruct xs as [|x xs]; iSimplifyEq.
   - wp_match. by iApply "HΦ".
@@ -42,11 +42,11 @@ Proof.
 Qed.
 
 Lemma rev_wp hd xs (Φ : val → iProp Σ) :
-  heap_ctx ∗ is_list hd xs ∗ (∀ w, is_list w (reverse xs) -∗ Φ w)
-  ⊢ WP rev hd (InjL #()) {{ Φ }}.
+  is_list hd xs -∗ (∀ w, is_list w (reverse xs) -∗ Φ w) -∗
+  WP rev hd (InjL #()) {{ Φ }}.
 Proof.
-  iIntros "(#Hh & Hxs & HΦ)".
-  iApply (rev_acc_wp hd NONEV xs [] with "[- $Hh $Hxs]").
-  iSplit; first done. iIntros (w). rewrite right_id_L. iApply "HΦ".
+  iIntros "Hxs HΦ".
+  iApply (rev_acc_wp hd NONEV xs [] with "Hxs [%]")=> //.
+  iIntros (w). rewrite right_id_L. iApply "HΦ".
 Qed.
 End list_reverse.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 0f7b99c73d6626db07d8240972e63209f0676d69..e504fcba61a93d673f2a87ccbfb259867a75c61f 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -29,18 +29,18 @@ Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
-Context `{!heapG Σ, !one_shotG Σ} (N : namespace) (HN : heapN ⊥ N).
+Context `{!heapG Σ, !one_shotG Σ} (N : namespace).
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
   (l ↦ NONEV ∗ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.
 
 Lemma wp_one_shot (Φ : val → iProp Σ) :
-  heap_ctx ∗ (∀ f1 f2 : val,
+  (∀ f1 f2 : val,
     (∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
     □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
-  iIntros "[#? Hf] /=".
+  iIntros "Hf /=".
   rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc Pending) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
@@ -83,14 +83,13 @@ Proof.
 Qed.
 
 Lemma ht_one_shot (Φ : val → iProp Σ) :
-  heap_ctx ⊢ {{ True }} one_shot_example #()
+  {{ True }} one_shot_example #()
     {{ ff,
       (∀ n : Z, {{ True }} Fst ff #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
       {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
     }}.
 Proof.
-  iIntros "#? !# _". iApply wp_one_shot. iSplit; first done.
-  iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
+  iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
   - iIntros (n) "!# _". wp_proj. iApply "Hf1".
   - iIntros "!# _". wp_proj.
     iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
diff --git a/tests/proofmode.v b/tests/proofmode.v
index df03e0f98087dafdf1f5008dbbb0188f1e85a676..833b8fdc1f88cfb0b2e870089be3e35f4e58f35a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
-  □ (P ∨ Q) ⊢ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
+  □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
   iIntros "#H #H2".
   (* should remove the disjunction "H" *)
@@ -37,8 +37,9 @@ Proof.
 Qed.
 
 Lemma demo_2 (M : ucmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M):
-    P2 ∗ (P3 ∗ Q) ∗ True ∗ P1 ∗ P2 ∗ (P4 ∗ (∃ x:nat, P5 x ∨ P3)) ∗ True
-  ⊢ P1 -∗ (True ∗ True) -∗ (((P2 ∧ False ∨ P2 ∧ ⌜0 = 0⌝) ∗ P3) ∗ Q ∗ P1 ∗ True) ∧
+  P2 ∗ (P3 ∗ Q) ∗ True ∗ P1 ∗ P2 ∗ (P4 ∗ (∃ x:nat, P5 x ∨ P3)) ∗ True -∗
+    P1 -∗ (True ∗ True) -∗
+  (((P2 ∧ False ∨ P2 ∧ ⌜0 = 0⌝) ∗ P3) ∗ Q ∗ P1 ∗ True) ∧
      (P2 ∨ False) ∧ (False → P5 0).
 Proof.
   (* Intro-patterns do something :) *)
@@ -54,17 +55,17 @@ Proof.
 Qed.
 
 Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) :
-  P1 ∗ P2 ∗ P3 ⊢ ▷ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
+  P1 ∗ P2 ∗ P3 -∗ ▷ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
 Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
 
 Definition foo {M} (P : uPred M) := (P → P)%I.
 Definition bar {M} : uPred M := (∀ P, foo P)%I.
 
-Lemma demo_4 (M : ucmraT) : True ⊢ @bar M.
+Lemma demo_4 (M : ucmraT) : True -∗ @bar M.
 Proof. iIntros. iIntros (P) "HP". done. Qed.
 
 Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
-  (∀ z, P → z ≡ y) ⊢ (P -∗ (x,x) ≡ (y,x)).
+  (∀ z, P → z ≡ y) -∗ (P -∗ (x,x) ≡ (y,x)).
 Proof.
   iIntros "H1 H2".
   iRewrite (uPred.internal_eq_sym x x with "[#]"); first done.
@@ -73,15 +74,15 @@ Proof.
 Qed.
 
 Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
-  True ⊢ ∀ x y z : nat,
-    ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x).
+  (∀ x y z : nat,
+    ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I.
 Proof.
   iIntros (a) "*".
   iIntros "#Hfoo **".
   by iIntros "# _".
 Qed.
 
-Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ∗ (Q1 ∧ Q2) ⊢ P ∗ Q1.
+Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
 Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
 
 Section iris.
@@ -91,7 +92,7 @@ Section iris.
 
   Lemma demo_8 N E P Q R :
     ↑N ⊆ E →
-    (True -∗ P -∗ inv N Q -∗ True -∗ R) ⊢ P -∗ ▷ Q ={E}=∗ R.
+    (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
   Proof.
     iIntros (?) "H HP HQ".
     iApply ("H" with "[#] HP >[HQ] >").
@@ -102,5 +103,5 @@ Section iris.
 End iris.
 
 Lemma demo_9 (M : ucmraT) (x y z : M) :
-  ✓ x → ⌜y ≡ z⌝ ⊢ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
+  ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
 Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 0f38392204e601f68c806ec3e93f897827f03030..ebca3662f90260bd0416c5ad814aa957d75c76da 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -34,11 +34,10 @@ Definition sum' : val := λ: "t",
   !"l".
 
 Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) :
-  heap_ctx ∗ l ↦ #n ∗ is_tree v t
-    ∗ (l ↦ #(sum t + n) -∗ is_tree v t -∗ Φ #())
-  ⊢ WP sum_loop v #l {{ Φ }}.
+  l ↦ #n -∗ is_tree v t -∗ (l ↦ #(sum t + n) -∗ is_tree v t -∗ Φ #()) -∗
+  WP sum_loop v #l {{ Φ }}.
 Proof.
-  iIntros "(#Hh & Hl & Ht & HΦ)".
+  iIntros "Hl Ht HΦ".
   iLöb as "IH" forall (v t l n Φ). wp_rec. wp_let.
   destruct t as [n'|tl tr]; simpl in *.
   - iDestruct "Ht" as "%"; subst.
@@ -55,12 +54,11 @@ Proof.
 Qed.
 
 Lemma sum_wp `{!heapG Σ} v t Φ :
-  heap_ctx ∗ is_tree v t ∗ (is_tree v t -∗ Φ #(sum t))
-  ⊢ WP sum' v {{ Φ }}.
+  is_tree v t -∗ (is_tree v t -∗ Φ #(sum t)) -∗ WP sum' v {{ Φ }}.
 Proof.
-  iIntros "(#Hh & Ht & HΦ)". rewrite /sum' /=.
+  iIntros "Ht HΦ". rewrite /sum' /=.
   wp_let. wp_alloc l as "Hl". wp_let.
-  wp_apply (sum_loop_wp with "[- $Hh $Ht $Hl]").
+  wp_apply (sum_loop_wp with "Hl Ht").
   rewrite Z.add_0_r.
   iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
 Qed.