diff --git a/_CoqProject b/_CoqProject
index 53a3c0def87690092e9eabc775cf6a11b59fdd07..3f01046c0098d6c83935edf7c423310d17da3f40 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -116,3 +116,4 @@ proofmode/invariants.v
 proofmode/weakestpre.v
 proofmode/ghost_ownership.v
 proofmode/sts.v
+proofmode/classes.v
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 3fa2eb41759ca5856e19802c49e557ed4fec5378..21e945304d7606384ab100e7cb485dae825121d6 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -698,8 +698,8 @@ End discrete.
 
 Notation discreteR A ra_mix :=
   (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
-Notation discreteLeibnizR A ra_mix :=
-  (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).
+Notation discreteUR A ra_mix ucmra_mix :=
+  (UCMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
 
 Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
   @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 843c10767ec9265f82e1c0931226df7a72bec2f0..068ec54b1907a4413779aded2f9c2ba588ad52cf 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -18,7 +18,6 @@ Context {A : Type} `{∀ x y : A, Decision (x = y)}.
 
 Instance dec_agree_valid : Valid (dec_agree A) := λ x,
   if x is DecAgree _ then True else False.
-Instance dec_agree_equiv : Equiv (dec_agree A) := equivL.
 Canonical Structure dec_agreeC : cofeT := leibnizC (dec_agree A).
 
 Instance dec_agree_op : Op (dec_agree A) := λ x y,
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 2c7b17090790ce889c1c5804a004b6aae3f53b13..3c8150335c516b2c975230625e30986f6567fa6d 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -46,8 +46,8 @@ Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
 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))) →
+  (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
+  (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
@@ -55,8 +55,8 @@ Proof.
 Qed.
 
 Lemma wp_lt E (n1 n2 : Z) P Φ :
-  (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  (n1 < n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
+  (n2 ≤ n1 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
@@ -64,8 +64,8 @@ Proof.
 Qed.
 
 Lemma wp_eq E (n1 n2 : Z) P Φ :
-  (n1 = n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
-  (n1 ≠ n2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+  (n1 = n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) →
+  (n1 ≠ n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) →
   P ⊢ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 84509a58b6a24859e569ac2169d217f9324ffaa9..a9dad272987643ed1ffb41ec4bd1763108e43596 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -148,81 +148,82 @@ Section heap.
   Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
 
   (** Weakest precondition *)
+  (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
   Lemma wp_alloc N E e v Φ :
     to_val e = Some v → nclose N ⊆ E →
-    heap_ctx N ★ ▷ (∀ l, l ↦ v -★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
+    heap_ctx N ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hinv Hheap". iIntros {h}. rewrite left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
     iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
-    iIntros {l} "[% Hheap]". iExists {[ l := (1%Qp, DecAgree v) ]}.
+    iIntros {l} "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
-    iFrame "Hheap". iSplit; first iPureIntro.
+    iFrame "Hheap". iSplitR; first iPureIntro.
     { by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
     iIntros "Hheap". iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
   Lemma wp_load N E l q v Φ :
     nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)
+    heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v)
     ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
     iIntros {?} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "> Hown". iExists _; iSplit; first done.
+    iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
     rewrite of_heap_singleton_op //. by iFrame.
   Qed.
 
   Lemma wp_store N E l v' e v Φ :
     to_val e = Some v → nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))
+    heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
+    iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
     { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
     rewrite of_heap_singleton_op //; eauto. by iFrame.
   Qed.
 
   Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
     to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))
+    heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     iIntros {????} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite of_heap_singleton_op //. iFrame "Hl".
-    iIntros "> Hown". iExists _; iSplit; first done.
+    iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
     rewrite of_heap_singleton_op //. by iFrame.
   Qed.
 
   Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
     to_val e1 = Some v1 → to_val e2 = Some v2 → nclose N ⊆ E →
-    heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))
+    heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     iIntros {???} "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
-    iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
+    iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
     { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
     rewrite of_heap_singleton_op //; eauto. by iFrame.
   Qed.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index fad80b689783cb411d70c812a993761b52a8627c..645347ed9e860958497881ee44fe655931ceaaf4 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -100,7 +100,7 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
   ⊢ WP newbarrier #() {{ Φ }}.
 Proof.
   iIntros {HN} "[#? HΦ]".
-  rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
+  rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
   iApply "HΦ".
   iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
   iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
@@ -127,7 +127,7 @@ Proof.
   rewrite /signal /send /barrier_ctx.
   iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
   iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
-  wp_store. destruct p; [|done].
+  wp_store. iPvsIntro. destruct p; [|done].
   iExists (State High I), (∅ : set token).
   iSplit; [iPureIntro; by eauto using signal_step|].
   iSplitR "HΦ"; [iNext|by auto].
@@ -143,7 +143,7 @@ Proof.
   iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
   iLöb as "IH". wp_rec. wp_focus (! _)%E.
   iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
-  wp_load. destruct p.
+  wp_load. iPvsIntro. destruct p.
   - (* a Low state. The comparison fails, and we recurse. *)
     iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
     { iNext. rewrite {2}/barrier_inv /=. by iFrame. }
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 3d88016457c22c581e3da8b4f5e84b39d80a0235..3edac7433880fda1fce7734d2f239f25ad68cec7 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -51,7 +51,7 @@ Lemma newlock_spec N (R : iProp) Φ :
   heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
 Proof.
   iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
-  wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
+  wp_seq. wp_alloc l as "Hl".
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
   iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
   { iIntros ">". iExists false. by iFrame. }
@@ -64,10 +64,10 @@ Proof.
   iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
   iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
   iInv N as { [] } "[Hl HR]".
-  - wp_cas_fail. iSplitL "Hl".
+  - wp_cas_fail. iPvsIntro; iSplitL "Hl".
     + iNext. iExists true; eauto.
     + wp_if. by iApply "IH".
-  - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
+  - wp_cas_suc. iPvsIntro. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
     + iNext. iExists true; eauto.
     + wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ; eauto.
 Qed.
@@ -77,6 +77,6 @@ Lemma release_spec R l (Φ : val → iProp) :
 Proof.
   iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
   rewrite /release. wp_let. iInv N as {b} "[Hl _]".
-  wp_store. iFrame "HΦ". iNext. iExists false. by iFrame.
+  wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
 Qed.
 End proof.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index ae36dc62eff66c336f585747efac051ec6249044..05e0f1cfecc5d44e9f70ea8c026b34a12cd52c3b 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -27,7 +27,8 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP par e {{ Φ }}.
 Proof.
-  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". rewrite /par. wp_value. wp_let. wp_proj.
+  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)".
+  rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
   wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
   iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
   iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 7ef95a18caf16265977ea8325fb7afdf9ca0ce5b..75a09b4422c3a3db8fc3a356227ff43ff3224a20 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -23,8 +23,7 @@ Class spawnG Σ := SpawnG {
 (** The functor we need. *)
 Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
 (* Show and register that they match. *)
-Instance inGF_spawnG
-  `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
+Instance inGF_spawnG `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
 Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
@@ -63,10 +62,10 @@ Proof.
   iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
   { iNext. iExists (InjLV #0). iFrame; eauto. }
   wp_apply wp_fork. iSplitR "Hf".
-  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
+  - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
   - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
     iInv N as {v'} "[Hl _]"; first wp_done.
-    wp_store. iSplit; [iNext|done].
+    wp_store. iPvsIntro; iSplit; [iNext|done].
     iExists (InjRV v); iFrame; eauto.
 Qed.
 
@@ -76,10 +75,10 @@ Proof.
   rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
   iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
-  - iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
+  - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
     wp_match. iApply ("IH" with "Hγ Hv").
   - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; simplify_eq/=.
-    + iSplitL "Hl Hγ".
+    + iPvsIntro; iSplitL "Hl Hγ".
       { iNext. iExists _; iFrame; eauto. }
       wp_match. by iApply "Hv".
     + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 3f2f3dffa66d0e92216a1558ec3a18b8f8c2cbb0..ea1e9076f1321ecbc02b81de65cc1fda023af8d5 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -25,7 +25,7 @@ Proof. exact: weakestpre.wp_bind. Qed.
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
   to_val e = Some v →
-  (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LitV (LitLoc l))))
+  ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
   ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   iIntros {?}  "[HP HΦ]".
@@ -41,7 +41,7 @@ Qed.
 
 Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
-  (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
     last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
@@ -49,7 +49,7 @@ Qed.
 
 Lemma wp_store_pst E σ l e v v' Φ :
   to_val e = Some v → σ !! l = Some v' →
-  (▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit)))
+  ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
   ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
   intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
@@ -58,7 +58,7 @@ Qed.
 
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
-  (▷ ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false)))
+  ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
   ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
@@ -68,7 +68,7 @@ Qed.
 
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
-  (▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV $ LitBool true)))
+  ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
   ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
@@ -78,18 +78,17 @@ 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 {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV LitUnit)) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
     last by intros; inv_head_step; eauto.
-  rewrite later_sep -(wp_value _ _ (Lit _)) //.
+  rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
 Qed.
 
 Lemma wp_rec E f x erec e1 e2 v2 Φ :
   e1 = Rec f x erec →
   to_val e2 = Some v2 →
-  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
-  ⊢ WP App e1 e2 @ E {{ Φ }}.
+  ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
   intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
     (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
@@ -98,18 +97,18 @@ Qed.
 
 Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →
-  ▷ Φ (LitV l') ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV l')) ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
-  ▷ Φ (LitV l') ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
   intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Φ :
@@ -128,18 +127,18 @@ Qed.
 
 Lemma wp_fst E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_snd E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
-    ?right_id -?wp_value //; intros; inv_head_step; eauto.
+    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_case_inl E e0 v0 e1 e2 Φ :
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 7d1113a18e573ff79e94cbcacd70db6261bcc066..8503a626fd70d265a747544e536f44e507f24076 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -22,7 +22,7 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
   IntoLaterEnvs Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
+    (Δ'' ⊢ |={E}=> Φ (LitV (LitLoc l)))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
@@ -36,7 +36,7 @@ Lemma tac_wp_load Δ Δ' N E i l q v Φ :
   (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ Φ v) →
+  (Δ' ⊢ |={E}=> Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
@@ -50,7 +50,8 @@ Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
   IntoLaterEnvs Δ Δ' →
   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 {{ Φ }}.
+  (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
+  Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
   rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -62,7 +63,7 @@ Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
   (Δ ⊢ heap_ctx N) → nclose N ⊆ E →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  (Δ' ⊢ Φ (LitV (LitBool false))) →
+  (Δ' ⊢ |={E}=> Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
@@ -76,7 +77,8 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
   IntoLaterEnvs Δ Δ' →
   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 {{ Φ }}.
+  (Δ'' ⊢ |={E}=> Φ (LitV (LitBool true))) →
+  Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros; subst.
   rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 17b76046dd3e3d26c85afed9ba251fe157a542f3..d32240a1ddb4b8224e63407669c0d34e16cf50fa 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -11,27 +11,34 @@ Ltac wp_bind K :=
 
 Ltac wp_done := rewrite /= ?to_of_val; fast_done.
 
-Ltac wp_value_head :=
-  match goal with
-  | |- _ ⊢ wp _ _ _ =>
-    etrans; [|eapply wp_value_pvs; wp_done]; lazy beta;
-    (* sometimes, we will have to do a final view shift, so only apply
-    pvs_intro if we obtain a consecutive wp *)
-    try (
-      etrans; [|apply pvs_intro];
-      match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
+(* sometimes, we will have to do a final view shift, so only apply
+pvs_intro if we obtain a consecutive wp *)
+Ltac wp_strip_pvs :=
+  lazymatch goal with
+  | |- _ ⊢ |={?E}=> _ =>
+    etrans; [|apply pvs_intro];
+    match goal with |- _ ⊢ wp E _ _ => simpl | _ => fail end
   end.
 
+Ltac wp_value_head := etrans; [|eapply wp_value_pvs; wp_done]; lazy beta.
+
 Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
 
 Ltac wp_seq_head :=
   lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q => etrans; [|eapply wp_seq; wp_done]; wp_strip_later
+  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+    etrans; [|eapply wp_seq; wp_done]; wp_strip_later
   end.
 
 Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val; try wp_strip_later; try wp_value_head);
-  repeat wp_seq_head.
+  rewrite /= ?to_of_val;
+  try wp_strip_later;
+  repeat lazymatch goal with
+  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+     etrans; [|eapply wp_seq; wp_done]; wp_strip_later
+  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
+  | |- _ ⊢ |={_}=> _ => wp_strip_pvs
+  end).
 
 Tactic Notation "wp_value" :=
   lazymatch goal with
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index ff70ca4dcfa6ed49a17c6a9306856fe91403b34d..0c243cf12d8af60a6bfc78cbb1eafc19b2407a69 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -39,7 +39,8 @@ Lemma wp_lift_atomic_head_step {E Φ} e1
   atomic e1 →
   head_reducible e1 σ1 →
   (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
+    ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_step. Qed.
 
@@ -48,7 +49,7 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
   head_reducible e1 σ1 →
   (∀ e2' σ2' ef', head_step e1 σ1 e2' σ2' ef' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 ef :
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 28a372fdfecd7f3f13e76a5bd0431d96ef45dcbc..843b5b883166abb395bddb0d2f19d0c6f46db755 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -66,7 +66,8 @@ Lemma wp_lift_atomic_step {E Φ} e1
   reducible e1 σ1 →
   (∀ e2 σ2 ef,
     prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
+    ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,
@@ -77,7 +78,7 @@ Proof.
   apply forall_intro=>ef; apply wand_intro_l.
   rewrite always_and_sep_l -assoc -always_and_sep_l.
   apply pure_elim_l=>-[[v2 Hv] ?] /=.
-  rewrite -pvs_intro.
+  rewrite -pvs_intro -wp_pvs.
   rewrite (forall_elim v2) (forall_elim σ2') (forall_elim ef) pure_equiv //.
   rewrite left_id wand_elim_r -(wp_value _ _ e2' v2) //.
   by erewrite of_to_val.
@@ -88,7 +89,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
   reducible e1 σ1 →
   (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef',
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') σ1) //.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index e7e517a6f700d38c2b373a9b06e244f17f0fadf3..c87539c436ddf75373b4c9501ea3c72c7f1a78b1 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -257,9 +257,11 @@ Lemma wp_strip_pvs E e P Φ :
 Proof. move=>->. by rewrite pvs_wp. Qed.
 Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊢ WP e @ E {{ Φ }}.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
+Lemma wp_value_pvs' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_pvs -wp_value'. Qed.
 Lemma wp_value_pvs E Φ e v :
   to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
-Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
+Proof. intros. rewrite -wp_pvs -wp_value //. Qed.
 Lemma wp_frame_l E e Φ R : R ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ★ Φ v }}.
 Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_step_r' E e Φ R :
diff --git a/proofmode/classes.v b/proofmode/classes.v
new file mode 100644
index 0000000000000000000000000000000000000000..b30f4311c5ca4cc0840a05f2bbad5867ffef12a5
--- /dev/null
+++ b/proofmode/classes.v
@@ -0,0 +1,312 @@
+From iris.algebra Require Export upred.
+From iris.algebra Require Import upred_big_op gmap upred_tactics.
+Import uPred.
+
+Section classes.
+Context {M : ucmraT}.
+Implicit Types P Q : uPred M.
+
+Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : □?p P ⊢ Q.
+Global Arguments from_assumption _ _ _ {_}.
+Global Instance from_assumption_exact p P : FromAssumption p P P.
+Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
+Global Instance from_assumption_always_l p P Q :
+  FromAssumption p P Q → FromAssumption p (□ P) Q.
+Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
+Global Instance from_assumption_always_r P Q :
+  FromAssumption true P Q → FromAssumption true P (□ Q).
+Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
+
+Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P ⊢ ■ φ.
+Global Arguments into_pure : clear implicits.
+Global Instance into_pure_pure φ : IntoPure (■ φ) φ.
+Proof. done. Qed.
+Global Instance into_pure_eq {A : cofeT} (a b : A) :
+  Timeless a → IntoPure (a ≡ b) (a ≡ b).
+Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
+Global Instance into_pure_valid `{CMRADiscrete A} (a : A) : IntoPure (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ → True ⊢ P.
+Global Arguments from_pure : clear implicits.
+Global Instance from_pure_pure φ : FromPure (■ φ) φ.
+Proof. intros ?. by apply pure_intro. Qed.
+Global Instance from_pure_eq {A : cofeT} (a b : A) : FromPure (a ≡ b) (a ≡ b).
+Proof. intros ->. apply eq_refl. Qed.
+Global Instance from_pure_valid {A : cmraT} (a : A) : FromPure (✓ a) (✓ a).
+Proof. intros ?. by apply valid_intro. Qed.
+
+Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
+Global Arguments into_persistentP : clear implicits.
+Global Instance into_persistentP_always_trans P Q :
+  IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
+Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
+Global Instance into_persistentP_always P : IntoPersistentP (â–¡ P) P | 1.
+Proof. done. Qed.
+Global Instance into_persistentP_persistent P :
+  PersistentP P → IntoPersistentP P P | 100.
+Proof. done. Qed.
+
+Class IntoLater (P Q : uPred M) := into_later : P ⊢ ▷ Q.
+Global Arguments into_later _ _ {_}.
+Class FromLater (P Q : uPred M) := from_later : ▷ Q ⊢ P.
+Global Arguments from_later _ _ {_}.
+
+Global Instance into_later_fallthrough P : IntoLater P P | 1000.
+Proof. apply later_intro. Qed.
+Global Instance into_later_later P : IntoLater (â–· P) P.
+Proof. done. Qed.
+Global Instance into_later_and P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∧ P2) (Q1 ∧ Q2).
+Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
+Global Instance into_later_or P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
+Global Instance into_later_sep P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ★ P2) (Q1 ★ Q2).
+Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
+
+Global Instance into_later_big_sepM `{Countable K} {A}
+    (Φ Ψ : K → A → uPred M) (m : gmap K A) :
+  (∀ x k, IntoLater (Φ k x) (Ψ k x)) →
+  IntoLater ([★ map] k ↦ x ∈ m, Φ k x) ([★ map] k ↦ x ∈ m, Ψ k x).
+Proof.
+  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
+Qed.
+Global Instance into_later_big_sepS `{Countable A}
+    (Φ Ψ : A → uPred M) (X : gset A) :
+  (∀ x, IntoLater (Φ x) (Ψ x)) →
+  IntoLater ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ x).
+Proof.
+  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
+Qed.
+
+Global Instance from_later_later P : FromLater (â–· P) P.
+Proof. done. Qed.
+Global Instance from_later_and P1 P2 Q1 Q2 :
+  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∧ P2) (Q1 ∧ Q2).
+Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
+Global Instance from_later_or P1 P2 Q1 Q2 :
+  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
+Global Instance from_later_sep P1 P2 Q1 Q2 :
+  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ★ P2) (Q1 ★ Q2).
+Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
+
+Class IntoWand (R P Q : uPred M) := into_wand : R ⊢ P -★ Q.
+Global Arguments into_wand : clear implicits.
+Global Instance into_wand_wand P Q : IntoWand (P -★ Q) P Q.
+Proof. done. Qed.
+Global Instance into_wand_impl P Q : IntoWand (P → Q) P Q.
+Proof. apply impl_wand. Qed.
+Global Instance into_wand_iff_l P Q : IntoWand (P ↔ Q) P Q.
+Proof. by apply and_elim_l', impl_wand. Qed.
+Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
+Proof. apply and_elim_r', impl_wand. Qed.
+Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
+Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
+
+Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P.
+Global Arguments from_and : clear implicits.
+
+Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
+Proof. done. Qed.
+Global Instance from_and_sep_persistent_l P1 P2 :
+  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2.
+Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
+Global Instance from_and_sep_persistent_r P1 P2 :
+  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2.
+Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
+Global Instance from_and_always P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
+Global Instance from_and_later P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
+
+Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 ★ Q2 ⊢ P.
+Global Arguments from_sep : clear implicits.
+
+Global Instance from_sep_sep P1 P2 : FromSep (P1 ★ P2) P1 P2 | 100.
+Proof. done. Qed.
+Global Instance from_sep_always P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
+Global Instance from_sep_later P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
+
+Global Instance from_sep_ownM (a b : M) :
+  FromSep (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
+Proof. by rewrite /FromSep ownM_op. Qed.
+Global Instance from_sep_big_sepM
+    `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
+  (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  FromSep ([★ map] k ↦ x ∈ m, Φ k x)
+    ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
+Proof.
+  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
+Qed.
+Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
+  (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
+  FromSep ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
+Proof.
+  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
+Qed.
+
+Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : □?p P ⊢ □?p (Q1 ★ Q2).
+Global Arguments into_sep : clear implicits.
+Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
+Global Arguments into_op {_} _ _ _ {_}.
+
+Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a â‹… b) a b.
+Proof. by rewrite /IntoOp. Qed.
+Global Instance into_op_persistent {A : cmraT} (a : A) :
+  Persistent a → IntoOp a a a.
+Proof. intros; apply (persistent_dup a). Qed.
+Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  IntoOp a b1 b2 → IntoOp a' b1' b2' →
+  IntoOp (a,a') (b1,b1') (b2,b2').
+Proof. by constructor. Qed.
+Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
+  IntoOp a b1 b2 → IntoOp (Some a) (Some b1) (Some b2).
+Proof. by constructor. Qed.
+
+Global Instance into_sep_sep p P Q : IntoSep p (P ★ Q) P Q.
+Proof. rewrite /IntoSep. by rewrite always_if_sep. Qed.
+Global Instance into_sep_ownM p (a b1 b2 : M) :
+  IntoOp a b1 b2 →
+  IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  rewrite /IntoOp /IntoSep=> ->. by rewrite ownM_op always_if_sep.
+Qed.
+
+Global Instance into_sep_and P Q : IntoSep true (P ∧ Q) P Q.
+Proof. by rewrite /IntoSep /= always_and_sep. Qed.
+Global Instance into_sep_and_persistent_l P Q :
+  PersistentP P → IntoSep false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
+Global Instance into_sep_and_persistent_r P Q :
+  PersistentP Q → IntoSep false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
+
+Global Instance into_sep_later p P Q1 Q2 :
+  IntoSep p P Q1 Q2 → IntoSep p (▷ P) (▷ Q1) (▷ Q2).
+Proof. by rewrite /IntoSep -later_sep !always_if_later=> ->. Qed.
+
+Global Instance into_sep_big_sepM
+    `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
+  (∀ k x, IntoSep p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  IntoSep p ([★ map] k ↦ x ∈ m, Φ k x)
+    ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
+Proof.
+  rewrite /IntoSep=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
+  by apply big_sepM_mono.
+Qed.
+Global Instance into_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
+  (∀ x, IntoSep p (Φ x) (Ψ1 x) (Ψ2 x)) →
+  IntoSep p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
+Proof.
+  rewrite /IntoSep=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
+  by apply big_sepS_mono.
+Qed.
+
+Class Frame (R P Q : uPred M) := frame : R ★ Q ⊢ P.
+Global Arguments frame : clear implicits.
+
+Global Instance frame_here R : Frame R R True.
+Proof. by rewrite /Frame right_id. Qed.
+
+Class MakeSep (P Q PQ : uPred M) := make_sep : P ★ Q ⊣⊢ PQ.
+Global Instance make_sep_true_l P : MakeSep True P P.
+Proof. by rewrite /MakeSep left_id. Qed.
+Global Instance make_sep_true_r P : MakeSep P True P.
+Proof. by rewrite /MakeSep right_id. Qed.
+Global Instance make_sep_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_sep_l R P1 P2 Q Q' :
+  Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ★ P2) Q' | 9.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
+Global Instance frame_sep_r R P1 P2 Q Q' :
+  Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10.
+Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
+
+Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
+Global Instance make_and_true_l P : MakeAnd True P P.
+Proof. by rewrite /MakeAnd left_id. Qed.
+Global Instance make_and_true_r P : MakeAnd P True P.
+Proof. by rewrite /MakeAnd right_id. Qed.
+Global Instance make_and_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_and_l R P1 P2 Q Q' :
+  Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
+Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+Global Instance frame_and_r R P1 P2 Q Q' :
+  Frame R P2 Q → MakeAnd P1 Q Q' → Frame R (P1 ∧ P2) Q' | 10.
+Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+
+Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
+Global Instance make_or_true_l P : MakeOr True P True.
+Proof. by rewrite /MakeOr left_absorb. Qed.
+Global Instance make_or_true_r P : MakeOr P True True.
+Proof. by rewrite /MakeOr right_absorb. Qed.
+Global Instance make_or_fallthrough P Q : MakeOr P Q (P ∨ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_or R P1 P2 Q1 Q2 Q :
+  Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
+Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
+
+Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
+Global Instance make_later_true : MakeLater True True.
+Proof. by rewrite /MakeLater later_True. Qed.
+Global Instance make_later_fallthrough P : MakeLater P (â–· P) | 100.
+Proof. done. Qed.
+
+Global Instance frame_later R P Q Q' :
+  Frame R P Q → MakeLater Q Q' → Frame R (▷ P) Q'.
+Proof.
+  rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
+Qed.
+
+Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
+Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+
+Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
+Global Arguments from_or : clear implicits.
+Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
+Proof. done. Qed.
+
+Class IntoOr P Q1 Q2 := into_or : P ⊢ Q1 ∨ Q2.
+Global Arguments into_or : clear implicits.
+Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
+Proof. done. Qed.
+Global Instance into_or_later P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
+
+Class FromExist {A} (P : uPred M) (Φ : A → uPred M) :=
+  from_exist : (∃ x, Φ x) ⊢ P.
+Global Arguments from_exist {_} _ _ {_}.
+Global Instance from_exist_exist {A} (Φ: A → uPred M): FromExist (∃ a, Φ a) Φ.
+Proof. done. Qed.
+
+Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
+  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
+Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
+
+Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
+  into_exist : P ⊢ ∃ x, Φ x.
+Global Arguments into_exist {_} _ _ {_}.
+Global Instance into_exist_exist {A} (Φ : A → uPred M) : IntoExist (∃ a, Φ a) Φ.
+Proof. done. Qed.
+Global Instance into_exist_later {A} P (Φ : A → uPred M) :
+  IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
+Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
+Global Instance into_exist_always {A} P (Φ : A → uPred M) :
+  IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
+End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 9611f7dcf7507f97354f63ad8ae6998f1ba3dafe..e35620930014910c450599f4688884f1663317ff 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export upred.
 From iris.algebra Require Import upred_big_op upred_tactics gmap.
-From iris.proofmode Require Export environments.
+From iris.proofmode Require Export environments classes.
 From iris.prelude Require Import stringmap hlist.
 Import uPred.
 
@@ -292,17 +292,6 @@ Proof.
 Qed.
 
 (** * Basic rules *)
-Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : □?p P ⊢ Q.
-Arguments from_assumption _ _ _ {_}.
-Global Instance from_assumption_exact p P : FromAssumption p P P.
-Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
-Global Instance from_assumption_always_l p P Q :
-  FromAssumption p P Q → FromAssumption p (□ P) Q.
-Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
-Global Instance from_assumption_always_r P Q :
-  FromAssumption true P Q → FromAssumption true P (□ Q).
-Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
-
 Lemma tac_assumption Δ i p P Q :
   envs_lookup i Δ = Some (p,P) → FromAssumption p P Q → Δ ⊢ Q.
 Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
@@ -327,35 +316,21 @@ Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
-Class IsPure (P : uPred M) (φ : Prop) := is_pure : P ⊣⊢ ■ φ.
-Arguments is_pure : clear implicits.
-Global Instance is_pure_pure φ : IsPure (■ φ) φ.
-Proof. done. Qed.
-Global Instance is_pure_eq {A : cofeT} (a b : A) :
-  Timeless a → IsPure (a ≡ b) (a ≡ b).
-Proof. intros; red. by rewrite timeless_eq. Qed.
-Global Instance is_pure_valid `{CMRADiscrete A} (a : A) : IsPure (✓ a) (✓ a).
-Proof. intros; red. by rewrite discrete_valid. Qed.
-
-Lemma tac_pure_intro Δ Q (φ : Prop) : IsPure Q φ → φ → Δ ⊢ Q.
-Proof. intros ->. apply pure_intro. Qed.
+Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ → φ → Δ ⊢ Q.
+Proof. intros ??. rewrite -(from_pure Q) //. apply True_intro. Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
-  envs_lookup_delete i Δ = Some (p, P, Δ') → IsPure P φ →
+  envs_lookup_delete i Δ = Some (p, P, Δ') → IntoPure P φ →
   (φ → Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
-  rewrite (is_pure P); by apply pure_elim_sep_l.
+  rewrite (into_pure P); by apply pure_elim_sep_l.
 Qed.
 
 Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ■ φ → Q) → (φ → Δ ⊢ Q).
 Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.
 
 (** * Later *)
-Class IntoLater (P Q : uPred M) := into_later : P ⊢ ▷ Q.
-Arguments into_later _ _ {_}.
-Class FromLater (P Q : uPred M) := from_later : ▷ Q ⊢ P.
-Arguments from_later _ _ {_}.
 Class IntoLaterEnv (Γ1 Γ2 : env (uPred M)) :=
   into_later_env : env_Forall2 IntoLater Γ1 Γ2.
 Class IntoLaterEnvs (Δ1 Δ2 : envs M) := {
@@ -363,47 +338,6 @@ Class IntoLaterEnvs (Δ1 Δ2 : envs M) := {
   into_later_spatial: IntoLaterEnv (env_spatial Δ1) (env_spatial Δ2)
 }.
 
-Global Instance into_later_fallthrough P : IntoLater P P | 1000.
-Proof. apply later_intro. Qed.
-Global Instance into_later_later P : IntoLater (â–· P) P.
-Proof. done. Qed.
-Global Instance into_later_and P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance into_later_or P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance into_later_sep P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ★ P2) (Q1 ★ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
-
-Global Instance into_later_big_sepM `{Countable K} {A}
-    (Φ Ψ : K → A → uPred M) (m : gmap K A) :
-  (∀ x k, IntoLater (Φ k x) (Ψ k x)) →
-  IntoLater ([★ map] k ↦ x ∈ m, Φ k x) ([★ map] k ↦ x ∈ m, Ψ k x).
-Proof.
-  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
-Qed.
-Global Instance into_later_big_sepS `{Countable A}
-    (Φ Ψ : A → uPred M) (X : gset A) :
-  (∀ x, IntoLater (Φ x) (Ψ x)) →
-  IntoLater ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ x).
-Proof.
-  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
-Qed.
-
-Global Instance from_later_later P : FromLater (â–· P) P.
-Proof. done. Qed.
-Global Instance from_later_and P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance from_later_or P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance from_later_sep P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ★ P2) (Q1 ★ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
-
 Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
 Proof. constructor. Qed.
 Global Instance into_later_env_snoc Γ1 Γ2 i P Q :
@@ -445,17 +379,6 @@ Qed.
 Lemma tac_always_intro Δ Q : envs_persistent Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
 Proof. intros. by apply: always_intro. Qed.
 
-Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
-Arguments into_persistentP : clear implicits.
-Global Instance into_persistentP_always_trans P Q :
-  IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
-Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
-Global Instance into_persistentP_always P : IntoPersistentP (â–¡ P) P | 1.
-Proof. done. Qed.
-Global Instance into_persistentP_persistent P :
-  PersistentP P → IntoPersistentP P P | 100.
-Proof. done. Qed.
-
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) → IntoPersistentP P P' →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
@@ -482,9 +405,9 @@ Proof.
   intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
   by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_impl_intro_pure Δ P φ Q : IsPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
+Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros. by apply impl_intro_l; rewrite (is_pure P); apply pure_elim_l.
+  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
 Qed.
 
 Lemma tac_wand_intro Δ Δ' i P Q :
@@ -500,24 +423,11 @@ Proof.
   intros. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_pure Δ P φ Q : IsPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
+Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
 Proof.
-  intros. by apply wand_intro_l; rewrite (is_pure P); apply pure_elim_sep_l.
+  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
 Qed.
 
-Class IntoWand (R P Q : uPred M) := into_wand : R ⊢ P -★ Q.
-Arguments into_wand : clear implicits.
-Global Instance into_wand_wand P Q : IntoWand (P -★ Q) P Q.
-Proof. done. Qed.
-Global Instance into_wand_impl P Q : IntoWand (P → Q) P Q.
-Proof. apply impl_wand. Qed.
-Global Instance into_wand_iff_l P Q : IntoWand (P ↔ Q) P Q.
-Proof. by apply and_elim_l', impl_wand. Qed.
-Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
-Proof. apply and_elim_r', impl_wand. Qed.
-Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
-Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
-
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
 Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
@@ -566,12 +476,12 @@ Qed.
 
 Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
-  IntoWand R P1 P2 → IsPure P1 φ →
+  IntoWand R P1 P2 → FromPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (into_wand R) (is_pure P1) pure_equiv // wand_True wand_elim_r.
+  by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
@@ -705,58 +615,10 @@ Proof.
 Qed.
 
 (** * Conjunction splitting *)
-Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P.
-Arguments from_and : clear implicits.
-
-Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
-Proof. done. Qed.
-Global Instance from_and_sep_persistent_l P1 P2 :
-  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2.
-Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
-Global Instance from_and_sep_persistent_r P1 P2 :
-  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2.
-Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
-Global Instance from_and_always P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
-Global Instance from_and_later P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
-
 Lemma tac_and_split Δ P Q1 Q2 : FromAnd P Q1 Q2 → (Δ ⊢ Q1) → (Δ ⊢ Q2) → Δ ⊢ P.
 Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
-Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 ★ Q2 ⊢ P.
-Arguments from_sep : clear implicits.
-
-Global Instance from_sep_sep P1 P2 : FromSep (P1 ★ P2) P1 P2 | 100.
-Proof. done. Qed.
-Global Instance from_sep_always P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
-Global Instance from_sep_later P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
-
-Global Instance from_sep_ownM (a b : M) :
-  FromSep (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
-Proof. by rewrite /FromSep ownM_op. Qed.
-Global Instance from_sep_big_sepM
-    `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
-  (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
-  FromSep ([★ map] k ↦ x ∈ m, Φ k x)
-    ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
-Proof.
-  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
-Qed.
-Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
-  (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
-  FromSep ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
-Proof.
-  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
-Qed.
-
 Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
   FromSep P Q1 Q2 →
   envs_split lr js Δ = Some (Δ1,Δ2) →
@@ -789,63 +651,6 @@ Proof.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
-Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : □?p P ⊢ □?p (Q1 ★ Q2).
-Arguments into_sep : clear implicits.
-Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
-Arguments into_op {_} _ _ _ {_}.
-
-Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a â‹… b) a b.
-Proof. by rewrite /IntoOp. Qed.
-Global Instance into_op_persistent {A : cmraT} (a : A) :
-  Persistent a → IntoOp a a a.
-Proof. intros; apply (persistent_dup a). Qed.
-Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
-  IntoOp a b1 b2 → IntoOp a' b1' b2' →
-  IntoOp (a,a') (b1,b1') (b2,b2').
-Proof. by constructor. Qed.
-Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
-  IntoOp a b1 b2 → IntoOp (Some a) (Some b1) (Some b2).
-Proof. by constructor. Qed.
-
-Global Instance into_sep_sep p P Q : IntoSep p (P ★ Q) P Q.
-Proof. rewrite /IntoSep. by rewrite always_if_sep. Qed.
-Global Instance into_sep_ownM p (a b1 b2 : M) :
-  IntoOp a b1 b2 →
-  IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  rewrite /IntoOp /IntoSep=> ->. by rewrite ownM_op always_if_sep.
-Qed.
-
-Global Instance into_sep_and P Q : IntoSep true (P ∧ Q) P Q.
-Proof. by rewrite /IntoSep /= always_and_sep. Qed.
-Global Instance into_sep_and_persistent_l P Q :
-  PersistentP P → IntoSep false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
-Global Instance into_sep_and_persistent_r P Q :
-  PersistentP Q → IntoSep false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
-
-Global Instance into_sep_later p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (▷ P) (▷ Q1) (▷ Q2).
-Proof. by rewrite /IntoSep -later_sep !always_if_later=> ->. Qed.
-
-Global Instance into_sep_big_sepM
-    `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
-  (∀ k x, IntoSep p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
-  IntoSep p ([★ map] k ↦ x ∈ m, Φ k x)
-    ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
-Proof.
-  rewrite /IntoSep=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
-  by apply big_sepM_mono.
-Qed.
-Global Instance into_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
-  (∀ x, IntoSep p (Φ x) (Ψ1 x) (Ψ2 x)) →
-  IntoSep p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
-Proof.
-  rewrite /IntoSep=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
-  by apply big_sepS_mono.
-Qed.
-
 Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoSep p P P1 P2 →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
@@ -856,70 +661,6 @@ Proof.
 Qed.
 
 (** * Framing *)
-Class Frame (R P Q : uPred M) := frame : R ★ Q ⊢ P.
-Arguments frame : clear implicits.
-
-Global Instance frame_here R : Frame R R True.
-Proof. by rewrite /Frame right_id. Qed.
-
-Class MakeSep (P Q PQ : uPred M) := make_sep : P ★ Q ⊣⊢ PQ.
-Global Instance make_sep_true_l P : MakeSep True P P.
-Proof. by rewrite /MakeSep left_id. Qed.
-Global Instance make_sep_true_r P : MakeSep P True P.
-Proof. by rewrite /MakeSep right_id. Qed.
-Global Instance make_sep_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
-Proof. done. Qed.
-Global Instance frame_sep_l R P1 P2 Q Q' :
-  Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ★ P2) Q' | 9.
-Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
-Global Instance frame_sep_r R P1 P2 Q Q' :
-  Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10.
-Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
-
-Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
-Global Instance make_and_true_l P : MakeAnd True P P.
-Proof. by rewrite /MakeAnd left_id. Qed.
-Global Instance make_and_true_r P : MakeAnd P True P.
-Proof. by rewrite /MakeAnd right_id. Qed.
-Global Instance make_and_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
-Proof. done. Qed.
-Global Instance frame_and_l R P1 P2 Q Q' :
-  Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
-Global Instance frame_and_r R P1 P2 Q Q' :
-  Frame R P2 Q → MakeAnd P1 Q Q' → Frame R (P1 ∧ P2) Q' | 10.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
-
-Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
-Global Instance make_or_true_l P : MakeOr True P True.
-Proof. by rewrite /MakeOr left_absorb. Qed.
-Global Instance make_or_true_r P : MakeOr P True True.
-Proof. by rewrite /MakeOr right_absorb. Qed.
-Global Instance make_or_fallthrough P Q : MakeOr P Q (P ∨ Q) | 100.
-Proof. done. Qed.
-Global Instance frame_or R P1 P2 Q1 Q2 Q :
-  Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
-Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
-
-Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
-Global Instance make_later_true : MakeLater True True.
-Proof. by rewrite /MakeLater later_True. Qed.
-Global Instance make_later_fallthrough P : MakeLater P (â–· P) | 100.
-Proof. done. Qed.
-
-Global Instance frame_later R P Q Q' :
-  Frame R P Q → MakeLater Q Q' → Frame R (▷ P) Q'.
-Proof.
-  rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
-Qed.
-
-Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
-  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
-Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
-  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
-Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
-
 Lemma tac_frame Δ Δ' i p R P Q :
   envs_lookup_delete i Δ = Some (p, R, Δ') → Frame R P Q →
   ((if p then Δ else Δ') ⊢ Q) → Δ ⊢ P.
@@ -930,24 +671,11 @@ Proof.
 Qed.
 
 (** * Disjunction *)
-Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
-Arguments from_or : clear implicits.
-Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
-Proof. done. Qed.
-
 Lemma tac_or_l Δ P Q1 Q2 : FromOr P Q1 Q2 → (Δ ⊢ Q1) → Δ ⊢ P.
 Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
 Lemma tac_or_r Δ P Q1 Q2 : FromOr P Q1 Q2 → (Δ ⊢ Q2) → Δ ⊢ P.
 Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
 
-Class IntoOr P Q1 Q2 := into_or : P ⊢ Q1 ∨ Q2.
-Arguments into_or : clear implicits.
-Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
-Proof. done. Qed.
-Global Instance into_or_later P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
-
 Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoOr P P1 P2 →
   envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
@@ -991,28 +719,6 @@ Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
 Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
 
 (** * Existential *)
-Class FromExist {A} (P : uPred M) (Φ : A → uPred M) :=
-  from_exist : (∃ x, Φ x) ⊢ P.
-Arguments from_exist {_} _ _ {_}.
-Global Instance from_exist_exist {A} (Φ: A → uPred M): FromExist (∃ a, Φ a) Φ.
-Proof. done. Qed.
-
-Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
-  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
-Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
-
-Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
-  into_exist : P ⊢ ∃ x, Φ x.
-Arguments into_exist {_} _ _ {_}.
-Global Instance into_exist_exist {A} (Φ : A → uPred M) : IntoExist (∃ a, Φ a) Φ.
-Proof. done. Qed.
-Global Instance into_exist_later {A} P (Φ : A → uPred M) :
-  IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
-Global Instance into_exist_always {A} P (Φ : A → uPred M) :
-  IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
-
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoExist P Φ →
   (∀ a, ∃ Δ',
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 86afa3f6b9fb6156a51c91eb8df1573bbe389ba2..20de4de2e2a8fd9684c974273d1e494b5462e4dc 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -7,6 +7,8 @@ Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 
+Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
+Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
 Global Instance from_assumption_pvs E p P Q :
   FromAssumption p P Q → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
@@ -179,3 +181,6 @@ Tactic Notation "iTimeless" constr(H) :=
 
 Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
   iTimeless H; iDestruct H as Hs.
+
+Hint Extern 2 (of_envs _ ⊢ _) =>
+  match goal with |- _ ⊢ (|={_}=> _)%I => iPvsIntro end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ab34269abacb2eca10904e5aa69fafed32ecbf8c..a3de35f17cfe8afb1edcab027762cab910c29cd1 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
 From iris.algebra Require Export upred.
-From iris.proofmode Require Export notation.
+From iris.proofmode Require Export classes notation.
 From iris.prelude Require Import stringmap hlist.
 
 Declare Reduction env_cbv := cbv [
@@ -112,13 +112,13 @@ Local Tactic Notation "iPersistent" constr(H) :=
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
-    |let P := match goal with |- IsPure ?P _ => P end in
+    |let P := match goal with |- IntoPure ?P _ => P end in
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
   eapply tac_pure_intro;
-    [let P := match goal with |- IsPure ?P _ => P end in
+    [let P := match goal with |- FromPure ?P _ => P end in
      apply _ || fail "iPureIntro:" P "not pure"|].
 
 (** * Specialize *)
@@ -184,7 +184,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
        eapply tac_specialize_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- IsPure ?Q _ => Q end in
+         |let Q := match goal with |- FromPure ?Q _ => Q end in
           apply _ || fail "iSpecialize:" Q "not pure"
          |env_cbv; reflexivity
          |(*goal*)
@@ -505,11 +505,11 @@ Tactic Notation "iNext":=
 Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
   [ (* (∀ _, _) *) apply tac_forall_intro; intros x
   | (* (?P → _) *) eapply tac_impl_intro_pure;
-     [let P := match goal with |- IsPure ?P _ => P end in
+     [let P := match goal with |- IntoPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   | (* (?P -★ _) *) eapply tac_wand_intro_pure;
-     [let P := match goal with |- IsPure ?P _ => P end in
+     [let P := match goal with |- IntoPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   |intros x].
diff --git a/tests/one_shot.v b/tests/one_shot.v
index e1b70e06a213b1e73f2abaebb6d05502442d5c5a..768662ea387d2fb1cfdefd31c4ee3ec49d0f5254 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -52,7 +52,7 @@ Proof.
   iPvsIntro. iApply "Hf"; iSplit.
   - iIntros {n} "!". wp_let.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
-    + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
+    + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft].
       iPvs (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
@@ -63,7 +63,7 @@ Proof.
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
       + iExists (InjLV #0). iFrame. eauto.
       + iExists (InjRV #m). iFrame. eauto. }
-    iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
+    iDestruct "Hv" as {v} "[Hl Hv]". wp_load; iPvsIntro.
     iAssert (one_shot_inv γ l ★ (v = InjLV #0 ∨ ∃ n : Z,
       v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "[$ #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
@@ -71,11 +71,11 @@ Proof.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     wp_let. iPvsIntro. iIntros "!". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
-    { wp_match. by iPvsIntro. }
+    { by wp_match. }
     wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
-    wp_load.
+    wp_load; iPvsIntro.
     iCombine "Hγ" "Hγ'" as "Hγ".
     iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; by eauto|].
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 24edb16fcc2af18a56fd0b6b817f4243e06c26e5..67eee7e4d9fe07540ddda92db0b872aa46ffca9d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -103,6 +103,6 @@ Section iris.
     iApply ("H" with "[#] HP |==>[HQ] |==>").
     - done.
     - by iApply inv_alloc.
-    - by iPvsIntro.
+    - done.
   Qed.
 End iris.