diff --git a/theories/base_logic/fix.v b/theories/base_logic/fix.v
index 717845fbca7db809265deaffe5ade6a376125a66..cbecbdc10857134ad7d5636d34365cb38e6853f9 100644
--- a/theories/base_logic/fix.v
+++ b/theories/base_logic/fix.v
@@ -40,8 +40,8 @@ Section least.
   Qed.
 
   Lemma uPred_least_fixpoint_ind (P : A → uPred M) (x : A) :
-    uPred_least_fixpoint F x -∗ □ (∀ y, F P y -∗ P y) -∗ P x.
-  Proof. iIntros "HF #HP". iApply "HF". done. Qed.
+    □ (∀ y, F P y -∗ P y) -∗ uPred_least_fixpoint F x -∗ P x.
+  Proof. iIntros "#HP HF". iApply "HF". done. Qed.
 End least.
 
 Section greatest.