diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index f474c5ffb63a8cd94bdf8ddf99a27a65e1185cc0..5d7196da856379911205639f543fa459dbdf057c 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -312,7 +312,7 @@ Section greatest_coind.
   Qed.
   Local Existing Instance paco_mono.
 
-  Lemma greatest_fixpoint_paco `{!NonExpansive Φ} :
+  Lemma greatest_fixpoint_paco (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, Φ y -∗ F (bi_greatest_fixpoint (λ Ψ a, Φ a ∨ F Ψ a)) y) -∗
     ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
   Proof using Type*.
diff --git a/tests/fixpoint.ref b/tests/fixpoint.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fixpoint.v b/tests/fixpoint.v
new file mode 100644
index 0000000000000000000000000000000000000000..b9e3c606fccd3026fbfdb45f9127c8726b2b965a
--- /dev/null
+++ b/tests/fixpoint.v
@@ -0,0 +1,29 @@
+From iris.bi Require Import lib.fixpoint.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+Section fixpoint.
+  Context {PROP : bi} `{!BiInternalEq PROP}
+    {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+
+  Definition L := bi_least_fixpoint F.
+  Definition G := bi_greatest_fixpoint F.
+
+  (* Make sure the lemmas [iApply] without having to repeat the induction
+  predicate [Φ]. See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/967
+  for details. *)
+  Lemma ind_test (a : A) :
+    ∀ x, L x -∗ x ≡ a.
+  Proof.
+    iApply (least_fixpoint_ind F); first by solve_proper. Undo.
+    iApply (least_fixpoint_ind_wf F); first by solve_proper. Undo.
+  Abort.
+
+  Lemma coind_test (a : A) :
+    ∀ x, x ≡ a -∗ G x.
+  Proof.
+    iApply (greatest_fixpoint_coind F); first by solve_proper. Undo.
+    iApply (greatest_fixpoint_paco F); first by solve_proper. Undo.
+  Abort.
+
+End fixpoint.