diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index a002baa5f2c3baa992d07bcfe7f1c4261d2eda00..fdff15b7bc34384c52a047245121dd65d85a2327 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -109,8 +109,8 @@ Proof.
     iSplit; [|done]. by iIntros "> ?". }
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { rewrite /barrier_ctx. by repeat iSplit. }
-  iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ★ sts_ownS γ' low_states {[Send]})%I with "[-]" as "[Hr Hs]".
+  iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
+    ★ sts_ownS γ' low_states {[Send]})%I with "=>[-]" as "[Hr Hs]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     + set_solver.
     + iApply (sts_own_weaken with "Hγ'");
@@ -148,7 +148,7 @@ Proof.
     iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
     { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
     iIntros "Hγ".
-    iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[Hγ]" as "Hγ".
+    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "=>[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext.
   - (* a High state: the comparison succeeds, and we perform a transition and
@@ -184,8 +184,8 @@ Proof.
   - iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
     iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
   - iIntros "Hγ".
-    iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
-      ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "[-]" as "[Hγ1 Hγ2]".
+    iAssert (sts_ownS γ (i_states i1) {[Change i1]}
+      ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "=>[-]" as "[Hγ1 Hγ2]".
     { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
       + set_solver.
       + iApply (sts_own_weaken with "Hγ");
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 938eecce3e7105066d4fa9a329df414bfdb4a643..3e2a5691fa06ebefb3659cc557568ff53101de44 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -494,24 +494,28 @@ Proof.
     by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js P1 P2 R Q :
+Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
+  to_assert : (R ★ (P -★ Q)) ⊢ Q.
+Global Arguments to_assert _ _ _ {_}.
+Lemma to_assert_fallthrough P Q : ToAssert P Q P.
+Proof. by rewrite /ToAssert wand_elim_r. Qed.
+
+Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  ToWand R P1 P2 →
+  ToWand R P1 P2 → ToAssert P1 Q P1' →
   ('(Δ1,Δ2) ← envs_split lr js Δ';
-    Δ2' ← envs_app (envs_persistent Δ1 && q) (Esnoc Enil j P2) Δ2;
+    Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  Δ1 ⊢ P1 → Δ2' ⊢ Q → Δ ⊢ Q.
+  Δ1 ⊢ P1' → Δ2' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ?? HP1 <-.
+  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
-  destruct (envs_persistent Δ1) eqn:?; simplify_eq/=.
-  - rewrite right_id (to_wand R) (persistentP Δ1) HP1.
-    by rewrite assoc (always_elim_if q) -always_if_sep wand_elim_l wand_elim_r.
-  - rewrite right_id (to_wand R).
-    by rewrite always_if_elim assoc HP1 wand_elim_l wand_elim_r.
+  rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
+  rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
+  by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
 Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
@@ -559,14 +563,15 @@ Proof.
   intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
 Qed.
 
-Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q :
+Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
+  ToAssert P Q R →
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  Δ1 ⊢ P → Δ2' ⊢ Q → Δ ⊢ Q.
+  Δ1 ⊢ R → Δ2' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ?? HP HQ. rewrite envs_split_sound //.
+  intros ??? HP HQ. rewrite envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
-  by rewrite right_id HP HQ wand_elim_r.
+  by rewrite right_id HP HQ.
 Qed.
 
 Lemma tac_assert_persistent Δ Δ' j P Q :
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index e9450cdaeabd10df827259552affa2c8672717b9..bf2b583845015649571cf22b832f5fe44d7878c3 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -31,7 +31,7 @@ Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
 Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
     (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
-  fsa_split : fsa E Φ ⊢ P;
+  fsa_split : fsa E Φ ⊣⊢ P;
   fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
 }.
 Global Arguments fsa_split {_} _ _ _ _ _ {_}.
@@ -42,6 +42,13 @@ Global Instance fsa_split_fsa {A} (fsa : FSA Λ Σ A) E Φ :
   FrameShiftAssertion fsaV fsa → FSASplit (fsa E Φ) E fsa fsaV Φ.
 Proof. done. Qed.
 
+Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
+  FSASplit Q E fsa fsaV Φ → ToAssert P Q (|={E}=> P).
+Proof.
+  intros.
+  by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
+Qed.
+
 Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → Δ ⊢ Q → Δ ⊢ |={E1,E2}=> Q.
 Proof. intros -> ->. apply pvs_intro. Qed.
 
@@ -87,17 +94,6 @@ Proof.
   intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
   eauto using tac_pvs_timeless.
 Qed.
-
-Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
-  FSASplit Q E fsa fsaV Φ →
-  envs_split lr js Δ = Some (Δ1,Δ2) →
-  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  Δ1 ⊢ (|={E}=> P) → Δ2' ⊢ fsa E Φ → Δ ⊢ Q.
-Proof.
-  intros ??? HP HQ. rewrite -(fsa_split Q) -fsa_pvs_fsa -HQ envs_split_sound //.
-  rewrite HP envs_app_sound //; simpl.
-  by rewrite right_id pvs_frame_r wand_elim_r.
-Qed.
 End pvs.
 
 Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
@@ -185,19 +181,3 @@ Tactic Notation "iTimeless" constr(H) :=
 
 Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
   iTimeless H; iDestruct H as Hs.
-
-Tactic Notation "iPvsAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
-  let H := iFresh in
-  let Hs := spec_pat.parse_one Hs in
-  lazymatch Hs with
-  | SGoal ?lr ?Hs =>
-     eapply tac_pvs_assert with _ _ _ _ _ _ lr Hs H Q _;
-       [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
-        apply _ || fail "iPvsAssert: " P "not a pvs"
-       |env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found"
-       |env_cbv; reflexivity|
-       |simpl; iDestruct H as pat]
-  | ?pat => fail "iPvsAssert: invalid pattern" pat
-  end.
-Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
-  iPvsAssert Q with "[]" as pat.
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index e3c065a657f66d3a6ba0d0d7969af1cf6b123240..c6919d5fa41cf24a3a21abba68856ed45021c0cb 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -1,7 +1,9 @@
 From iris.prelude Require Export strings.
 
+Inductive spec_goal_kind := GoalStd | GoalPvs.
+
 Inductive spec_pat :=
-  | SGoal : bool → list string → spec_pat
+  | SGoal : spec_goal_kind → bool → list string → spec_pat
   | SGoalPersistent : spec_pat
   | SGoalPure : spec_pat
   | SName : bool → string → spec_pat (* first arg = persistent *)
@@ -15,7 +17,8 @@ Inductive token :=
   | TBracketR : token
   | TPersistent : token
   | TPure : token
-  | TForall : token.
+  | TForall : token
+  | TPvs : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -29,13 +32,14 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
   | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
+  | String "=" (String ">" s) => tokenize_go s (TPvs :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
 Inductive state :=
   | StTop : state
-  | StAssert : bool → list string → state.
+  | StAssert : spec_goal_kind → bool → list string → state.
 
 Fixpoint parse_go (ts : list token) (s : state)
     (k : list spec_pat) : option (list spec_pat) :=
@@ -46,16 +50,18 @@ Fixpoint parse_go (ts : list token) (s : state)
      | TName s :: ts => parse_go ts StTop (SName false s :: k)
      | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
      | TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
-     | TBracketL :: ts => parse_go ts (StAssert false []) k
+     | TBracketL :: ts => parse_go ts (StAssert GoalStd false []) k
+     | TPvs :: TBracketL :: ts => parse_go ts (StAssert GoalPvs false []) k
+     | TPvs :: ts => parse_go ts StTop (SGoal GoalPvs true [] :: k)
      | TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
      | TForall :: ts => parse_go ts StTop (SForall :: k)
      | _ => None
      end
-  | StAssert neg ss =>
+  | StAssert kind neg ss =>
      match ts with
-     | TMinus :: ts => guard (¬neg ∧ ss = []); parse_go ts (StAssert true ss) k
-     | TName s :: ts => parse_go ts (StAssert neg (s :: ss)) k
-     | TBracketR :: ts => parse_go ts StTop (SGoal neg (rev ss) :: k)
+     | TMinus :: ts => guard (¬neg ∧ ss = []); parse_go ts (StAssert kind true ss) k
+     | TName s :: ts => parse_go ts (StAssert kind neg (s :: ss)) k
+     | TBracketR :: ts => parse_go ts StTop (SGoal kind neg (rev ss) :: k)
      | _ => None
      end
   end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 195995bfc4a96ac7554ccaed2b433578d0d57aa1..17fc75871491231339be2c155df269d0ed0c4f8a 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -186,10 +186,11 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |env_cbv; reflexivity
          |(*goal*)
          |go H1 pats]
-    | SGoal ?lr ?Hs :: ?pats =>
-       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _;
+    | SGoal ?k ?lr ?Hs :: ?pats =>
+       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
+         |match k with GoalStd => apply to_assert_fallthrough | GoalPvs => apply _ end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
          |(*goal*)
          |go H1 pats]
@@ -225,24 +226,25 @@ Tactic Notation "iPoseProof" open_constr(t) :=
   let H := iFresh in iPoseProof t as H.
 
 (** * Apply *)
-Tactic Notation "iApplyCore" constr(H) := first
-  [iExact H
-  |eapply tac_apply with _ H _ _ _;
-     [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
-     |apply _ || fail 1 "iApply: cannot apply" H|]].
-
 Tactic Notation "iApply" open_constr(t) :=
+  let finish H := first
+    [iExact H
+    |eapply tac_apply with _ H _ _ _;
+       [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
+       |let P := match goal with |- ToWand ?P _ _ => P end in
+        apply _ || fail 1 "iApply: cannot apply" H ":" P
+       |lazy beta (* reduce betas created by instantiation *)]] in
   let Htmp := iFresh in
   lazymatch t with
   | ITrm ?H ?xs ?pat =>
      iPoseProofCore H as Htmp; last (
        iSpecializeArgs Htmp xs;
        try (iSpecializeArgs Htmp (hcons _ _));
-       iSpecializePat Htmp pat; last iApplyCore Htmp)
+       iSpecializePat Htmp pat; last finish Htmp)
   | _ =>
      iPoseProofCore t as Htmp; last (
        try (iSpecializeArgs Htmp (hcons _ _));
-       iApplyCore Htmp)
+       finish Htmp)
   end; try apply _.
 
 (** * Revert *)
@@ -703,18 +705,21 @@ Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
-  | [SGoal ?lr ?Hs] =>
-     eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *)
-       [env_cbv; reflexivity || fail "iAssert:" Hs "not found"
-       |env_cbv; reflexivity|
-       |iDestructHyp H as pat]
-  | [SGoalPersistent]  =>
+  | [SGoalPersistent] =>
      eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
-       [apply _ || fail "iAssert:" Q "not persistent"
+       [env_cbv; reflexivity
+       |(*goal*)
+       |apply _ || fail "iAssert:" Q "not persistent"
+       |iDestructHyp H as pat]
+  | [SGoal ?k ?lr ?Hs] =>
+     eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
+       [match k with GoalStd => apply to_assert_fallthrough | GoalPvs => apply _ end
+       |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
        |env_cbv; reflexivity|
        |iDestructHyp H as pat]
   | ?pat => fail "iAssert: invalid pattern" pat
   end.
+
 Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
   iAssert Q with "[]" as pat.
 
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 0dec14048af6494247fdd8a38c691fc081b573a8..a74ee879ef6b374e1d0f1217f00cae1741114951 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.
+From iris.proofmode Require Import pviewshifts invariants.
 
 Lemma demo_0 {M : cmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
@@ -83,13 +83,26 @@ Qed.
 
 Section iris.
   Context {Λ : language} {Σ : iFunctor}.
+  Implicit Types E : coPset.
+  Implicit Types P Q : iProp Λ Σ.
 
-  Lemma demo_7 (E1 E2 E : coPset) (P : iProp Λ Σ) :
+  Lemma demo_7 E1 E2 E P :
     E1 ⊆ E2 → E ⊆ E1 →
     (|={E1,E}=> ▷ P) ⊢ (|={E2,E ∪ E2 ∖ E1}=> ▷ P).
   Proof.
     iIntros {? ?} "Hpvs".
-    iPvs "Hpvs"; first (split_and?; set_solver).
+    iPvs "Hpvs"; first set_solver.
     done.
   Qed.
+
+  Lemma demo_8 N E P Q R :
+    nclose N ⊆ E →
+    (True -★ P -★ inv N Q -★ True -★ R) ⊢ (P -★ ▷ Q -★ |={E}=> R).
+  Proof.
+    iIntros {?} "H HP HQ".
+    iApply ("H" with "[#] HP =>[HQ] =>").
+    - done.
+    - by iApply inv_alloc.
+    - by iPvsIntro.
+  Qed.
 End iris.