diff --git a/_CoqProject b/_CoqProject
index 1a100843dc5b2fc1c01ce77e4da3220ad3c04994..6f18679ede63cf8188fd34628bd7404382ced25c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -116,15 +116,11 @@ tests/list_reverse.v
 tests/tree_sum.v
 tests/counter.v
 proofmode/coq_tactics.v
-proofmode/pviewshifts.v
 proofmode/environments.v
 proofmode/intro_patterns.v
 proofmode/spec_patterns.v
 proofmode/sel_patterns.v
 proofmode/tactics.v
 proofmode/notation.v
-proofmode/invariants.v
-proofmode/weakestpre.v
-proofmode/ghost_ownership.v
 proofmode/classes.v
 proofmode/class_instances.v
diff --git a/algebra/auth.v b/algebra/auth.v
index cd2a8b3265256d40c5bf989f55954e7291ec182c..d831c60814efde52431787db4ea8e2c133ffbe50 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export excl local_updates.
 From iris.algebra Require Import upred updates.
+From iris.proofmode Require Import class_instances.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
@@ -224,6 +225,14 @@ End cmra.
 Arguments authR : clear implicits.
 Arguments authUR : clear implicits.
 
+(* Proof mode class instances *)
+Instance from_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
+  FromOp a b1 b2 → FromOp (◯ a) (◯ b1) (◯ b2).
+Proof. done. Qed.
+Instance into_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
+  IntoOp a b1 b2 → IntoOp (◯ a) (◯ b1) (◯ b2).
+Proof. done. Qed.
+
 (* Functor *)
 Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
   Auth (excl_map f <$> authoritative x) (f (auth_own x)).
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 474b1af4109e549e3da8a257d5fae1f897859af0..79a64561af3e1874c16f986a6a0aefddd422d67b 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1208,8 +1208,8 @@ Section option.
 
   Lemma Some_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
   Proof. rewrite option_included; naive_solver. Qed.
-  Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
-  Proof. rewrite Some_included; naive_solver. Qed.
+  Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≼ y.
+  Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
   Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
   Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
 End option.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index da126ca99a9fa35ba1b94cb84d083f44072c4a42..f3ab299c94438473d271cdbdb996679983e43950 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -450,6 +450,36 @@ Proof.
     by apply prodC_map_ne; apply cFunctor_contractive.
 Qed.
 
+Instance compose_ne {A} {B B' : cofeT} (f : B -n> B') n :
+  Proper (dist n ==> dist n) (compose f : (A -c> B) → A -c> B').
+Proof. intros g g' Hf x; simpl. by rewrite (Hf x). Qed.
+
+Definition cofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
+  @CofeMor (_ -c> _) (_ -c> _) (compose f) _.
+Instance cofe_funC_map_ne {A B B'} n :
+  Proper (dist n ==> dist n) (@cofe_funC_map A B B').
+Proof. intros f f' Hf g x. apply Hf. Qed.
+
+Program Definition cofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := cofe_funC T (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := cofe_funC_map (cFunctor_map F fg)
+|}.
+Next Obligation.
+  intros ?? A1 A2 B1 B2 n ???; by apply cofe_funC_map_ne; apply cFunctor_ne.
+Qed.
+Next Obligation. intros F1 F2 A B ??. by rewrite /= /compose /= !cFunctor_id. Qed.
+Next Obligation.
+  intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
+  by rewrite !cFunctor_compose.
+Qed.
+
+Instance cofe_funCF_contractive (T : Type) (F : cFunctor) :
+  cFunctorContractive F → cFunctorContractive (cofe_funCF T F).
+Proof.
+  intros ?? A1 A2 B1 B2 n ???;
+    by apply cofe_funC_map_ne; apply cFunctor_contractive.
+Qed.
+
 Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
   cFunctor_map A1 A2 B1 B2 fg :=
@@ -759,6 +789,7 @@ Qed.
 
 (** Notation for writing functors *)
 Notation "∙" := idCF : cFunctor_scope.
+Notation "T -c> F" := (cofe_funCF T%type F%CF) : cFunctor_scope.
 Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
 Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
 Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
diff --git a/algebra/frac.v b/algebra/frac.v
index 6bd8528ebc899307ab7ec8f5f8a0902cbb3c5f4f..11cb32deab537850a9a6977cd4e385dab7f04ccd 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -35,6 +35,3 @@ Global Instance frac_full_exclusive : Exclusive 1%Qp.
 Proof.
   move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
 Qed.
-
-Lemma invalid_plus_q: ∀ (q: Qp), ¬ ✓ (1 + q)%Qp.
-Proof. intros q H. by apply (Qp_ge_1 q). Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 5005e73cf4b3d9d881110f7ea9ad6554bfdf1a16..a0b70717465f4bd0844d2286384e8737ff29a7fc 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1361,6 +1361,12 @@ Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. uPred.unseal. by destruct mx. Qed.
 
+(* Functions *)
+Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof. by uPred.unseal. Qed.
+Lemma cofe_moreC_equivI {A B : cofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof. by uPred.unseal. Qed.
+
 (* Timeless instances *)
 Global Instance pure_timeless φ : TimelessP (■ φ : uPred M)%I.
 Proof.
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 89990989d5a81b261b795a6498c9819173e489dd..a5c116b0b47b4a442b3e5a154962cea0449f9f31 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.program_logic Require Import auth ownership.
 From iris.heap_lang Require Import proofmode notation.
-From iris.proofmode Require Import tactics weakestpre.
+From iris.proofmode Require Import tactics.
 
 Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang].
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 58f5b61924321becad297793af05a164a721af66..11f538b90a1df728df488309130a7f3fed1b236e 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -2,7 +2,7 @@ From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import upred_big_op gmap frac dec_agree.
 From iris.program_logic Require Export invariants ghost_ownership.
 From iris.program_logic Require Import ownership auth.
-From iris.proofmode Require Import weakestpre.
+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
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index f318d1b6b13382341ad04e3419b5b773bffdd3c8..96769c478f0c081dcbdfdb10937bdeb72ed18f20 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index ce437f6ca59ab00fdcc75726fc64d343da63542d..05a04531406c768fcb0439744c94cff394193231 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 138568fff3fd615d19ae62038364aabcf2241661..71db1619931284c0285b8252ce106204cdb6ad25 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 From iris.heap_lang.lib Require Import lock.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index d4994cd762b91c116fb7ff35a469ee55bfa672cb..157b85465214314825309b46187a2e4b925500fa 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth gset.
 From iris.heap_lang.lib Require Export lock.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 3c8b7494f90c50cc69872b9dc4441b901fb2c511..278165adb0f0d324b009188c8d92aa6ada6c45ee 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import tactics.
 From iris.prelude Require Import fin_maps.
 Import uPred.
 
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 1a0a66e79a9fafeab5e9c49694b3407742e6219d..9e07d30d9becb5290b7c20e2cb69df0301ca6feb 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -1,5 +1,6 @@
+From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export weakestpre.
+From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export wp_tactics heap.
 Import uPred.
 
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 9d0b2e481abae93db713df70621cd5baf723f093..f54b034357e9e87642ff26744038ee179e6f61c9 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -567,9 +567,12 @@ Proof.
   apply Qp_eq; simpl. ring.
 Qed.
 
-Lemma Qp_ge_1 (q: Qp): ¬ ((1 + q)%Qp ≤ 1%Qp)%Qc.
+Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp ≤ 1%Qp)%Qc.
 Proof.
   intros Hle.
   apply (Qcplus_le_mono_l q 0 1) in Hle.
-  apply Qcle_ngt in Hle. by destruct q.
+  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
 Qed.
+
+Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
+Proof. apply Qclt_le_weak, Qp_prf. Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 5569939f7e2b865bfcc8675ecc0276f5cb8f6a3f..4b6540a71517af9c68ceca1c731d4a7bcbff075c 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
 From iris.program_logic Require Import ownership.
-From iris.proofmode Require Import tactics weakestpre.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 99231ad4b0cf0597d3aba06bb77d80627a66e656..d8a586dbee791e35334a1a899001c7581c64ebf6 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,7 +1,7 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index fc41df57d5bc47f9a1e3ae9eb83b3b0f73ccff2f..f5ea2bb994f955b475c3c54ba75f0c93cd932ca5 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Import auth gmap agree upred_big_op.
-From iris.proofmode Require Import tactics invariants.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 (** The CMRAs we need. *)
diff --git a/program_logic/cancelable_invariants.v b/program_logic/cancelable_invariants.v
index a7fadea600fa017fc4d7b568f25e6ad70d044be7..486f22b641f793dc61b075b826cfffef7a680334 100644
--- a/program_logic/cancelable_invariants.v
+++ b/program_logic/cancelable_invariants.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export invariants.
 From iris.algebra Require Export frac.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 0c35491a598320365077a68331d4ecbd3164f033..b43ead95ec2738b2795f44de64500150735a1ecd 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -1,7 +1,7 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.program_logic Require Import ownership.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import tactics.
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 721feaa00a23b165e00ba54bd28cc962c808e73c..dc9840967502ae4acb56d30f00f2e58304ef9abb 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export model.
 From iris.algebra Require Import iprod gmap.
+From iris.proofmode Require Import classes.
 Import uPred.
 
 (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
@@ -145,3 +146,16 @@ Proof.
   - apply cmra_transport_valid, ucmra_unit_valid.
   - intros x; destruct inG_prf. by rewrite left_id.
 Qed.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{inG Σ A}.
+  Implicit Types a b : A.
+
+  Global Instance into_and_own p γ a b1 b2 :
+    IntoOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
+  Global Instance from_sep_own γ a b1 b2 :
+    FromOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
+End proofmode_classes.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 817a21e295c66caeb711b88f17ce6c2d22be4a35..912f193a0453b2acdb67303a0f4ca6af0b6fb3b9 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre viewshifts.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import tactics.
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index ca670bf1bf1eec7cff02d5bfc26489169f537b35..08b7407aeafa4ff9a41f59e2199bf451ec8b75bc 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Export namespaces.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import pviewshifts.
+From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
@@ -61,3 +61,29 @@ Proof.
   iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
 Qed.
 End inv.
+
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
+  let Htmp := iFresh in
+  let patback := intro_pat.parse_one Hclose in
+  let pat := constr:(IList [[IName Htmp; patback]]) in
+  iVs (inv_open _ N with "[#]") as pat;
+    [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
+    [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
+    |tac Htmp].
+
+Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1 x2) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1 x2 x3) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1 x2 x3 x4) pat) Hclose.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 16ef16d2ab251d56e2c66554f9021767519c8542..c27eea3e8f5b08ab6ba71a5f9ddfb872f790fd7b 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Export upred_big_op.
-From iris.proofmode Require Import pviewshifts.
+From iris.proofmode Require Import tactics.
 
 Section lifting.
 Context `{irisG Λ Σ}.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index efe52436687caf2b04514c40139f7d33d9fd14f3..6af5bfac1e4b633a7e89222bc4f7c63495042be9 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export iris.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
-From iris.proofmode Require Import ghost_ownership tactics.
+From iris.proofmode Require Import tactics.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
   to_agree (Next (iProp_unfold P)).
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 971cbaa6050a82577111fa180ab2807877a1c847..540074e9ca6354f5b967761a439fb583a240326b 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export iris.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Import upred_big_op gmap.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics classes.
 Import uPred.
 
 Program Definition pvs_def `{irisG Λ Σ}
@@ -136,3 +136,54 @@ Proof.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
 Qed.
 End pvs.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{irisG Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+
+  Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
+  Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
+
+  Global Instance from_assumption_pvs E p P Q :
+    FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.
+  Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.
+
+  Global Instance into_wand_pvs E1 E2 R P Q :
+    IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+  Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
+
+  Global Instance from_sep_pvs E P Q1 Q2 :
+    FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
+  Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
+
+  Global Instance or_split_pvs E1 E2 P Q1 Q2 :
+    FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
+  Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
+
+  Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Σ) :
+    FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
+  Proof.
+    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+  Qed.
+
+  Global Instance frame_pvs E1 E2 R P Q :
+    Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+  Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
+
+  Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
+  Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
+
+  Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
+  Proof. by rewrite /FromVs -rvs_pvs. Qed.
+
+  Global Instance elim_vs_rvs_pvs E1 E2 P Q :
+    ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+  Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
+  Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
+    ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+  Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
+End proofmode_classes.
+
+Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) =>
+  match goal with |- _ ⊢ |={_}=> _ => iVsIntro end.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index a27c28ce626975b1f37f8fa5642ef1b9c4a85445..5163df44663199104b91bb16ebdcc632b71df6c6 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Export sts.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 (** The CMRA we need. *)
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index d3126bf039879f208136c7e9d9201b3d50aaffd5..5be913c45bd7ad13e529f8982b9b6eb64f1faf68 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -1,5 +1,6 @@
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Definition tlN : namespace := nroot .@ "tl".
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index d7b188265fdc0767296004247b2ecc4db74eef99..13a286abb4d8a7a7f021bef08356d73bd79ed810 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,5 +1,5 @@
-From iris.program_logic Require Export pviewshifts.
-From iris.proofmode Require Import pviewshifts invariants.
+From iris.program_logic Require Export invariants.
+From iris.proofmode Require Import tactics.
 
 Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P → |={E1,E2}=> Q))%I.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 432700e1566f697338c938b2d5001ad0c049e54a..9c8d93f85ad43402a71c975d9ec62f2bae3f6950 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
-From iris.proofmode Require Import tactics pviewshifts.
+From iris.proofmode Require Import tactics classes.
 Import uPred.
 
 Definition wp_pre `{irisG Λ Σ}
@@ -211,3 +211,32 @@ Lemma wp_wand_r E e Φ Ψ :
   WP e @ E {{ Φ }} ★ (∀ v, Φ v -★ Ψ v) ⊢ WP e @ E {{ Ψ }}.
 Proof. by rewrite comm wp_wand_l. Qed.
 End wp.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{irisG Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : val Λ → iProp Σ.
+
+  Global Instance frame_wp E e R Φ Ψ :
+    (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
+
+  Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
+  Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
+
+  Global Instance elim_vs_rvs_wp E e P Φ :
+    ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
+
+  Global Instance elim_vs_pvs_wp E e P Φ :
+    ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
+
+  (* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
+  Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
+    atomic e →
+    ElimVs (|={E1,E2}=> P) P
+           (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+  Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
+End proofmode_classes.
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index e193dd85a4ee2de8aa1b40ea4415dcc6874b9e74..47277f8bbb07e719a210cbb259d19bf7f5dca5bb 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -132,6 +132,10 @@ Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
 (* FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ★ P2) P1 P2 | 100.
 Proof. done. Qed.
+Global Instance from_sep_ownM (a b1 b2 : M) :
+  FromOp a b1 b2 →
+  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /FromSep -ownM_op from_op. 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.
@@ -142,9 +146,6 @@ Global Instance from_sep_rvs P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
 Proof. rewrite /FromSep=><-. apply rvs_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)) →
@@ -160,6 +161,20 @@ Proof.
   rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
 Qed.
 
+(* FromOp *)
+Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a â‹… b) a b.
+Proof. by rewrite /FromOp. Qed.
+Global Instance from_op_persistent {A : cmraT} (a : A) :
+  Persistent a → FromOp a a a.
+Proof. intros. by rewrite /FromOp -(persistent_dup a). Qed.
+Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  FromOp a b1 b2 → FromOp a' b1' b2' →
+  FromOp (a,a') (b1,b1') (b2,b2').
+Proof. by constructor. Qed.
+Global Instance from_op_Some {A : cmraT} (a : A) b1 b2 :
+  FromOp a b1 b2 → FromOp (Some a) (Some b1) (Some b2).
+Proof. by constructor. Qed.
+
 (* IntoOp *)
 Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a â‹… b) a b.
 Proof. by rewrite /IntoOp. Qed.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index ac65c81e3c600675c27a64f1724a6670a80eeb4f..224b1e48338410d8a3088648ce4c3d66d133c7ca 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -39,6 +39,9 @@ Global Arguments into_and : clear implicits.
 Lemma mk_into_and_sep p P Q1 Q2 : (P ⊢ Q1 ★ Q2) → IntoAnd p P Q1 Q2.
 Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
 
+Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1 ⋅ b2 ≡ a.
+Global Arguments from_op {_} _ _ _ {_}.
+
 Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
 Global Arguments into_op {_} _ _ _ {_}.
 
@@ -70,5 +73,8 @@ Global Arguments from_vs : clear implicits.
 
 Class ElimVs (P P' : uPred M) (Q Q' : uPred M) :=
   elim_vs : P ★ (P' -★ Q') ⊢ Q.
-Arguments elim_vs _ _ _ _ {_}.
+Global Arguments elim_vs _ _ _ _ {_}.
+
+Lemma elim_vs_dummy P Q : ElimVs P P Q Q.
+Proof. by rewrite /ElimVs wand_elim_r. Qed.
 End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 867ba424ed222514fcc2cf314090897927488c7e..4c270ef4083e38d2349d006ce65963e43641060d 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -531,17 +531,9 @@ Proof.
     by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
 Qed.
 
-Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
-  into_assert : R ★ (P -★ Q) ⊢ Q.
-Global Arguments into_assert _ _ _ {_}.
-Lemma into_assert_default P Q : IntoAssert P Q P.
-Proof. by rewrite /IntoAssert wand_elim_r. Qed.
-Global Instance to_assert_rvs P Q : IntoAssert P (|=r=> Q) (|=r=> P).
-Proof. by rewrite /IntoAssert rvs_frame_r wand_elim_r rvs_trans. Qed.
-
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  IntoWand R P1 P2 → IntoAssert P1 Q P1' →
+  IntoWand R P1 P2 → ElimVs P1' P1 Q Q →
   ('(Δ1,Δ2) ← envs_split lr js Δ';
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
@@ -553,7 +545,7 @@ Proof.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
   rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
-  rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
+  rewrite -(elim_vs P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
   by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
@@ -614,11 +606,11 @@ Proof.
   by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
 Qed.
 
-Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
-  IntoAssert P Q R →
+Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
+  ElimVs P' P Q Q →
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  (Δ1 ⊢ R) → (Δ2' ⊢ Q) → Δ ⊢ Q.
+  (Δ1 ⊢ P') → (Δ2' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP HQ. rewrite envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
diff --git a/proofmode/ghost_ownership.v b/proofmode/ghost_ownership.v
deleted file mode 100644
index a1a2804ed8db7286ab15f047b6bebb2fcfc5c206..0000000000000000000000000000000000000000
--- a/proofmode/ghost_ownership.v
+++ /dev/null
@@ -1,15 +0,0 @@
-From iris.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export tactics.
-From iris.program_logic Require Export ghost_ownership.
-
-Section ghost.
-Context `{inG Σ A}.
-Implicit Types a b : A.
-
-Global Instance into_and_own p γ a b1 b2 :
-  IntoOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
-Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
-Global Instance from_sep_own γ a b :
-  FromSep (own γ (a ⋅ b)) (own γ a) (own γ b) | 90.
-Proof. by rewrite /FromSep own_op. Qed.
-End ghost.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
deleted file mode 100644
index d5813093ec389667f2a166db0f299c1b7b0a712e..0000000000000000000000000000000000000000
--- a/proofmode/invariants.v
+++ /dev/null
@@ -1,29 +0,0 @@
-From iris.proofmode Require Export tactics pviewshifts.
-From iris.program_logic Require Export invariants.
-From iris.proofmode Require Import coq_tactics intro_patterns.
-
-Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
-  let Htmp := iFresh in
-  let patback := intro_pat.parse_one Hclose in
-  let pat := constr:(IList [[IName Htmp; patback]]) in
-  iVs (inv_open _ N with "[#]") as pat;
-    [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
-    [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
-    |tac Htmp].
-
-Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1 x2) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1 x2 x3) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1 x2 x3 x4) pat) Hclose.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
deleted file mode 100644
index ecdc794a5e363a601bcd071abc5292d00f6ecdb1..0000000000000000000000000000000000000000
--- a/proofmode/pviewshifts.v
+++ /dev/null
@@ -1,58 +0,0 @@
-From iris.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export tactics ghost_ownership.
-From iris.program_logic Require Export pviewshifts.
-Import uPred.
-
-Section pvs.
-Context `{irisG Λ Σ}.
-Implicit Types P Q : iProp Σ.
-
-Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
-Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
-
-Global Instance from_assumption_pvs E p P Q :
-  FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.
-Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.
-
-Global Instance into_wand_pvs E1 E2 R P Q :
-  IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
-Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
-
-Global Instance from_sep_pvs E P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
-Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
-
-Global Instance or_split_pvs E1 E2 P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
-Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
-
-Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Σ) :
-  FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
-Proof.
-  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
-
-Global Instance frame_pvs E1 E2 R P Q :
-  Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
-Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
-
-Global Instance to_assert_pvs E1 E2 P Q :
-  IntoAssert P (|={E1,E2}=> Q) (|={E1}=> P).
-Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_trans. Qed.
-
-Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
-Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
-
-Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
-Proof. by rewrite /FromVs -rvs_pvs. Qed.
-
-Global Instance elim_vs_rvs_pvs E1 E2 P Q :
-  ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
-Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
-Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
-  ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
-Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
-End pvs.
-
-Hint Extern 2 (of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ |={_}=> _ => iVsIntro end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 217ec83a62041863e05ce6cbaff8d83bedaa694c..c63a655e1b9d3f06b9c3c6886ea170f0e8580b4d 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -312,7 +312,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |match vs with
-          | false => apply into_assert_default
+          | false => apply elim_vs_dummy
           | true => apply _ || fail "iSpecialize: cannot generate view shifted goal"
           end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
@@ -1099,7 +1099,7 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
   | [SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs)] =>
      eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
        [match vs with
-        | false => apply into_assert_default
+        | false => apply elim_vs_dummy
         | true => apply _ || fail "iAssert: cannot generate view shifted goal"
         end
        |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
@@ -1133,7 +1133,10 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
     eapply (tac_rewrite _ Heq _ _ lr);
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |let P := match goal with |- ?P ⊢ _ => P end in
-       reflexivity || fail "iRewrite:" P "not an equality"
+       (* use ssreflect apply: which is better at dealing with unification
+       involving canonical structures. This is useful for the COFE canonical
+       structure in uPred_eq that it may have to infer. *)
+       apply: reflexivity || fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
 
@@ -1146,7 +1149,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |env_cbv; reflexivity || fail "iRewrite:" H "not found"
       |let P := match goal with |- ?P ⊢ _ => P end in
-       reflexivity || fail "iRewrite:" P "not an equality"
+       apply: reflexivity || fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity
       |env_cbv; reflexivity|lazy beta; iClear Heq]).
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
deleted file mode 100644
index 90b01fb5c434365d6abef7081b09ff403f679f74..0000000000000000000000000000000000000000
--- a/proofmode/weakestpre.v
+++ /dev/null
@@ -1,36 +0,0 @@
-From iris.proofmode Require Export classes pviewshifts.
-From iris.proofmode Require Import coq_tactics.
-From iris.program_logic Require Export weakestpre.
-Import uPred.
-
-Section weakestpre.
-Context `{irisG Λ Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val Λ → iProp Σ.
-
-Global Instance frame_wp E e R Φ Ψ :
-  (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
-Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
-
-Global Instance to_assert_wp E e P Φ :
-  IntoAssert P (WP e @ E {{ Ψ }}) (|={E}=> P).
-Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_wp. Qed.
-
-Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
-Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
-
-Global Instance elim_vs_rvs_wp E e P Φ :
-  ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
-Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
-
-Global Instance elim_vs_pvs_wp E e P Φ :
-  ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
-Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
-
-(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
-Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
-  atomic e →
-  ElimVs (|={E1,E2}=> P) P
-         (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
-Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
-End weakestpre.
diff --git a/tests/atomic.v b/tests/atomic.v
index a26f9ee60e422adbe23299f222e75ee95aa913a5..0b978bab802c84dd816be2935cbb01692c1d8457 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
-From iris.proofmode Require Import tactics pviewshifts weakestpre.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Section atomic.
@@ -42,7 +42,6 @@ Section atomic.
 End atomic.
 
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.proofmode Require Import invariants.
 
 Section incr.
   Context `{!heapG Σ} (N : namespace).
diff --git a/tests/counter.v b/tests/counter.v
index 8d5bb62c1b5b1fe3a1cfb6497a8d3c26de647bf9..92d7c61c2adb7e26f98d400cbad62e4adf589e37 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -5,7 +5,7 @@ under max can be found in `heap_lang/lib/counter.v`. *)
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.program_logic Require Export hoare.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 78adb9719af808df78da53ccabbe052c2db0b042..3aa32e4ffb922f8538495872b2300bc8f01734ac 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
 From iris.heap_lang.lib.barrier Require Import proof specification.
 From iris.heap_lang Require Import notation par proofmode.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 
 Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
   csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 92598f56215fafe323dfe9a0dd1e933d9f5d0aec..1bf2188437a272fd0c680466356beb0c0605b8d8 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl dec_agree csum.
 From iris.heap_lang Require Import assert proofmode notation.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 496993c030520b6e58bc187841f25ef73adee074..73f1f0a830b892dfdbe97822d260c58ef89c7d36 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.proofmode Require Import pviewshifts invariants.
+From iris.program_logic Require Import invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ (∀ x, x = 0 ∨ x = 1) → (Q ∨ P).