diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index f4da0ed786ded955e152a2d499e932b067b69484..380e71fa9205f110d31d3e294a1f90f75c877714 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1240,8 +1240,7 @@ Local Ltac iApplyHypLoop H :=
     [eapply tac_apply with H _ _ _;
       [pm_reflexivity
       |iSolveTC
-      |pm_reduce;
-       pm_prettify (* reduce redexes created by instantiation *)]
+      |pm_reduce]
     |iSpecializePat H "[]"; last iApplyHypLoop H].
 
 Tactic Notation "iApplyHyp" constr(H) :=
@@ -1253,7 +1252,9 @@ Tactic Notation "iApplyHyp" constr(H) :=
      end].
 
 Tactic Notation "iApply" open_constr(lem) :=
-  iPoseProofCore lem as false (fun H => iApplyHyp H).
+  iPoseProofCore lem as false (fun H => iApplyHyp H);
+  pm_prettify. (* reduce redexes created by instantiation; this is done at the
+  very end after all type classes have been solved. *)
 
 (** * Disjunction *)
 Tactic Notation "iLeft" :=
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ce21d1c9d1c2c3b7629c0e461fa8a4ff09977bb1..9a7ac3b30cf08e677bf850d288606e5c85ce1e04 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -385,6 +385,18 @@ No applicable tactic.
   "HP" : default emp mP
   --------------------------------------∗
   default emp mP
+"test_iApply_prettification3"
+     : string
+1 goal
+  
+  PROP : bi
+  Ψ, Φ : nat → PROP
+  HP : ∀ (f : nat → nat) (y : nat),
+         TCEq f (λ x : nat, x + 10) → Ψ (f 1) -∗ Φ y
+  ============================
+  "H" : Ψ 11
+  --------------------------------------∗
+  Ψ (1 + 10)
 1 goal
   
   PROP : bi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8ad3f6da4b95f11a1f86e15748228e9556d8b504..d67a8b9d11264a7f481add5aad2c7df33a31fd6e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1109,6 +1109,17 @@ Proof.
   iIntros "?". iExists _. iApply modal_if_lemma2. done.
 Qed.
 
+Check "test_iApply_prettification3".
+Lemma test_iApply_prettification3 (Ψ Φ : nat → PROP) :
+  (∀ f y, TCEq f (λ x, x + 10) → Ψ (f 1) -∗ Φ y) →
+  Ψ 11 -∗ Φ 10.
+Proof.
+  iIntros (HP) "H".
+  iApply HP.
+  Show.
+  iApply "H".
+Qed.
+
 Lemma test_iDestruct_clear P Q R :
   P -∗ (Q ∗ R) -∗ True.
 Proof.