diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index f5da06eeb72a8691a733689c19af06b4f6c5e9d3..6804c1720ada7d964251c4185682b2b26f4b684d 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -233,7 +233,7 @@ Section fixpoint.
   Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
 
   Lemma fixpoint_ind (P : A → Prop) :
-    Proper ((≡) ==> iff) P →
+    Proper ((≡) ==> impl) P →
     (∃ x, P x) → (∀ x, P x → P (f x)) →
     (∀ (c : chain A), (∀ n, P (c n)) → P (compl c)) →
     P (fixpoint f).