diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 300a460748407a49e5e5eea3fd407a11e0feb047..e4bae919c7e08d267a52323a87fd25d29f4383b0 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..d2935202396c1ca67b6f16235480a800ee3b1c0f
--- /dev/null
+++ b/tests/fixpoint.v
@@ -0,0 +1,27 @@
+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 apply without having to repeat the induction predicate [Φ]. *)
+  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.