diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index efc72d90924eb84a0d2213bc8869ef6803800f2d..4449a272b5a39953f5061fca252cd53ce909ddab 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -27,6 +27,14 @@ Proof. intros. by rewrite /FromBare bare_elim. Qed.
 Global Instance from_bare_default P : FromBare (â–  P) P | 100.
 Proof. by rewrite /FromBare. Qed.
 
+(* IntoSink *)
+Global Instance into_sink_True : @IntoSink PROP True emp | 0.
+Proof. by rewrite /IntoSink -sink_True_emp sink_pure. Qed.
+Global Instance into_sink_absorbing P : Absorbing P → IntoSink P P | 1.
+Proof. intros. by rewrite /IntoSink absorbing_sink. Qed.
+Global Instance into_sink_default P : IntoSink (â–² P) P | 100.
+Proof. by rewrite /IntoSink. Qed.
+
 (* FromAssumption *)
 Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
 Proof. by rewrite /FromAssumption /= bare_persistently_if_elim. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 7263098d0b512c55eb1454bb22b1e5883e82a8b5..ca815691fa66cf6d09e5f38b81a4d2d9a9a99eac 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -68,6 +68,12 @@ Arguments from_bare {_} _%I _%type_scope {_}.
 Hint Mode FromBare + ! - : typeclass_instances.
 Hint Mode FromBare + - ! : typeclass_instances.
 
+Class IntoSink {PROP : bi} (P Q : PROP) := into_sink : P ⊢ ▲ Q.
+Arguments IntoSink {_} _%I _%I.
+Arguments into_sink {_} _%I _%I {_}.
+Hint Mode IntoSink + ! -  : typeclass_instances.
+Hint Mode IntoSink + - ! : typeclass_instances.
+
 Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
   into_internal_eq : P ⊢ x ≡ y.
 Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 3697b33f6ab49d9ced67dcade192e3ef4a5413d9..a555a196b19d23bc0c7698e33cc07d82c16e2a25 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -684,18 +684,20 @@ Proof.
   by rewrite emp_wand wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
+Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P1' P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand q true R P1 P2 →
   Persistent P1 →
+  IntoSink P1' P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
-  (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
+  (Δ' ⊢ P1') → (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+  intros [? ->]%envs_lookup_delete_Some ???? HP1 <-.
   rewrite envs_lookup_sound //.
   rewrite -(idemp bi_and (envs_delete _ _ _)).
   rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
-  rewrite {1}HP1 (persistent_persistently_2 P1) persistently_and_bare_sep_l assoc.
+  rewrite {1}HP1 (into_sink P1') (persistent_persistently_2 P1) sink_persistently.
+  rewrite persistently_and_bare_sep_l assoc.
   rewrite -bare_persistently_if_idemp -bare_persistently_idemp.
   rewrite (bare_persistently_bare_persistently_if q) bare_persistently_if_sep_2.
   by rewrite into_wand wand_elim_l wand_elim_r.
@@ -703,20 +705,18 @@ Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
-  (Δ ⊢ R) →
+  (Δ ⊢ ▲ R) →
   IntoPersistent false R R' →
-  (if q then TCTrue else TCAnd (PositiveBI PROP) (Affine R)) →
+  (if q then TCTrue else AffineBI PROP) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
   (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
-  - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R).
+  - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R) sink_persistently.
+    by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
+  - rewrite (absorbing_sink R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
     by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
-  - destruct Hpos.
-    rewrite -(affine_bare R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
-    rewrite bare_and_lr bare_sep sep_elim_r bare_elim.
-    by rewrite persistently_and_bare_sep_l wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4329266a730ef82f9bee5db3e3b1bf8a9825489b..c6c174b992889fada6a645622bd15f4e83def522 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -459,12 +459,13 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          |done_if d (*goal*)
          |go H1 pats]
     | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
-       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
+       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _ _;
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |apply _ ||
           let Q := match goal with |- Persistent ?Q => Q end in
           fail "iSpecialize:" Q "not persistent"
+         |apply _
          |env_reflexivity
          |iFrame Hs_frame; done_if d (*goal*)
          |go H1 pats]
@@ -535,7 +536,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
       lazymatch eval compute in
         (p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
       | true =>
-         (* FIXME: do something reasonable when the BI is not positive *)
+         (* FIXME: do something reasonable when the BI is not affine *)
          eapply tac_specialize_persistent_helper with _ H _ _ _ _;
            [env_reflexivity || fail "iSpecialize:" H "not found"
            |iSpecializePat H pat; last (iExact H)