diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 51b84fa2780eb1656983403b535c8672e80e4708..6cbde74af585b88184beb7098640ccd525d82a3c 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -578,13 +578,13 @@ Tactic failure: iStartProof: not a BI assertion.
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
 "iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (constr) as (tactic3)" and
-"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
-Tactic failure: iPoseProof: not a BI assertion.
+"iPoseProofCoreLem (open_constr) as (tactic3)" and 
+"iIntoEmpValid", last call failed.
+Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
 "iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
+"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
 fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
 fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
 fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
@@ -604,7 +604,7 @@ Tactic failure: iPoseProof: "Hx" not found.
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
 "iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
+"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
 fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
 fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
 fun Htmp =>
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 3e76db3856b0ec7596dc7f675781aa34746627ce..5a17f50ce18ecd626ff43bad57954a1dc936938f 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -271,7 +271,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
-    iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox").
+    iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
   - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ -279,7 +279,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
-    iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox").
+    iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
 Qed.
 
@@ -296,14 +296,14 @@ Proof.
     iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
-    iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox").
+    iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
   - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
     iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
     iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
     iExists γ. iIntros "{$% $#} !>". iNext.
-    iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox").
+    iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
 End box.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 7f096f398cd6f59542a8c05923a647e917519e27..8e1a9e59adbb61ea7a5d17770180f5c0ad4c9e6d 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -95,7 +95,8 @@ Proof. iApply saved_anything_alloc. Qed.
 Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
   saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
 Proof.
-  iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
+  iIntros "HP HQ". iApply later_equivI.
+  iApply (saved_anything_agree (F := ▶ ∙) with "HP HQ").
 Qed.
 
 (* Saved predicates. *)
@@ -129,6 +130,6 @@ Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
   saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
 Proof.
   unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
-  iDestruct (saved_anything_agree with "HΦ HΨ") as "Heq".
+  iDestruct (saved_anything_agree (F := A -d> ▶ ∙) with "HΦ HΨ") as "Heq".
   by iDestruct (discrete_fun_equivI with "Heq") as "?".
 Qed.
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 1423040d92826018c0680a2ca337180a353e6299..df9083d3074b13826f3a8b456384cae00c85d1ff 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -108,7 +108,7 @@ Section greatest.
     F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
   Proof.
     iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
-    iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
+    iSplit; last done. iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
     iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
   Qed.
 
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 72164546d98a8543aff55a8d13f9c82daa233844..62c1402606a8fff084c31f2c905e61cbe76d8bca 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -452,8 +452,19 @@ Proof.
   by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
 Qed.
 
-Lemma tac_pose_proof Δ j P Q :
-  P →
+Definition IntoEmpValid (φ : Type) (P : PROP) := φ → bi_emp_valid P.
+Lemma into_emp_valid_here φ P : AsEmpValid φ P → IntoEmpValid φ P.
+Proof. by intros [??]. Qed.
+Lemma into_emp_valid_impl (φ ψ : Type) P :
+  φ → IntoEmpValid ψ P → IntoEmpValid (φ → ψ) P.
+Proof. rewrite /IntoEmpValid; auto. Qed.
+Lemma into_emp_valid_forall {A} (φ : A → Type) P x :
+  IntoEmpValid (φ x) P → IntoEmpValid (∀ x : A, φ x) P.
+Proof. rewrite /IntoEmpValid; auto. Qed.
+
+Lemma tac_pose_proof Δ j (φ : Prop) P Q :
+  φ →
+  IntoEmpValid φ P →
   match envs_app true (Esnoc Enil j P) Δ with
   | None => False
   | Some Δ' => envs_entails Δ' Q
@@ -461,8 +472,8 @@ Lemma tac_pose_proof Δ j P Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
-  rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=.
-  by rewrite -HP /= intuitionistically_emp emp_wand.
+  rewrite envs_entails_eq => ? HP <-. rewrite envs_app_singleton_sound //=.
+  by rewrite -HP //= intuitionistically_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ i j Q :
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index fbde9ca80de9cf704c3f7da69bf0efa094d89c34..915b812d0c9f43e916734946815f65064394d27a 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -720,58 +720,9 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
   (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
 Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
 
-(* The tactic [iIntoEmpValid] tactic solves a goal [bi_emp_valid ?Q]. The
-argument [t] must be a Coq term whose type is of the following shape:
-
-[∀ (x_1 : A_1) .. (x_n : A_n), φ]
-
-for which we have an instance [AsEmpValid φ ?Q].
-
-Examples of such [φ]s are
-
-- [bi_emp_valid P], in which case [Q] is unified with [P].
-- [P1 ⊢ P2], in which case [Q] is unified with [P1 -∗ P2].
-- [P1 ⊣⊢ P2], in which case [Q] is unified with [P1 ↔ P2].
-
-The tactic instantiates each dependent argument [x_i : A_i] with an evar and
-generates a goal [A_i] for each non-dependent argument [x_i : A_i].
-
-For example, if the initial goal is [bi_emp_valid ?Q] and [t] has type
-[∀ x, P x → R x], then it generates an evar [?x] for [x], a subgoal [P ?x],
-and unifies [?Q] with [R x]. *)
-Local Ltac iIntoEmpValid t :=
-  let go_specialize t tT :=
-    lazymatch tT with                (* We do not use hnf of tT, because, if
-                                        entailment is not opaque, then it would
-                                        unfold it. *)
-    | ?P → ?Q => let H := fresh in assert P as H; [|iIntoEmpValid uconstr:(t H); clear H]
-    | ∀ _ : ?T, _ =>
-      (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
-      (* This is a workarround for Coq bug #6583. *)
-      let e := fresh in evar (e:id T);
-      let e' := eval unfold e in e in clear e; iIntoEmpValid (t e')
-    end
-  in
-    (* We try two reduction tactics for the type of t before trying to
-       specialize it. We first try the head normal form in order to
-       unfold all the definition that could hide an entailment.  Then,
-       we try the much weaker [eval cbv zeta], because entailment is
-       not necessarilly opaque, and could be unfolded by [hnf].
-
-       However, for calling type class search, we only use [cbv zeta]
-       in order to make sure we do not unfold [bi_emp_valid]. *)
-    let tT := type of t in
-    first
-      [ let tT' := eval hnf in tT in go_specialize t tT'
-      | let tT' := eval cbv zeta in tT in go_specialize t tT'
-      | let tT' := eval cbv zeta in tT in
-        notypeclasses refine (as_emp_valid_1 tT _ _);
-          [iSolveTC || fail 1 "iPoseProof: not a BI assertion"
-          |exact t]].
-
 Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
   let Δ := iGetCtx in
-  eapply tac_pose_proof_hyp with H Hnew;
+  notypeclasses refine (tac_pose_proof_hyp _ H Hnew _ _);
     pm_reduce;
     lazymatch goal with
     | |- False =>
@@ -787,10 +738,47 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
     | _ => idtac
     end.
 
-Tactic Notation "iPoseProofCoreLem" constr(lem) "as" tactic3(tac) :=
+(* The tactic [iIntoEmpValid] tactic "imports a Coq lemma into the proofmode",
+i.e. it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
+following shape:
+
+[∀ (x_1 : A_1) .. (x_n : A_n), φ]
+
+for which we have an instance [AsEmpValid φ ?Q].
+
+Examples of such [φ]s are
+
+- [bi_emp_valid P], in which case [?Q] is unified with [P].
+- [P1 ⊢ P2], in which case [?Q] is unified with [P1 -∗ P2].
+- [P1 ⊣⊢ P2], in which case [?Q] is unified with [P1 ↔ P2].
+
+The tactic instantiates each dependent argument [x_i : A_i] with an evar, and
+generates a goal [A_i] for each non-dependent argument [x_i : A_i].
+
+For example, if goal is [bi_emp_valid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
+[iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
+[?Q] with [R1 ?x -∗ R2 ?x]. *)
+Ltac iIntoEmpValid_go := first
+  [(* Case [φ → ψ] *)
+   notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
+     [(*goal for [φ] *)|iIntoEmpValid_go]
+  |(* Case [∀ x : A, φ] *)
+   notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
+  |(* Case [P ⊢ Q], [P ⊣⊢ Q], [bi_emp_valid P] *)
+   notypeclasses refine (into_emp_valid_here _ _ _)].
+
+Ltac iIntoEmpValid :=
+  (* Factor out the base case of the loop to avoid needless backtracking *)
+  iIntoEmpValid_go;
+    [.. (* goals for premises *)
+    |iSolveTC ||
+     let φ := lazymatch goal with |- AsEmpValid ?φ _ => φ end in
+     fail "iPoseProof:" φ "not a BI assertion"].
+
+Tactic Notation "iPoseProofCoreLem" open_constr(lem) "as" tactic3(tac) :=
   let Hnew := iFresh in
-  eapply tac_pose_proof with Hnew _; (* (j:=H) *)
-    [iIntoEmpValid lem
+  notypeclasses refine (tac_pose_proof _ Hnew _ _ _ lem _ _);
+    [iIntoEmpValid
     |pm_reduce;
      lazymatch goal with
      | |- False =>