diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.fst
index 0d3a43e27..a0a5293e3 100644
--- a/hax-lib/proofs/fstar/extraction/Hax_lib.fst
+++ b/hax-lib/proofs/fstar/extraction/Hax_lib.fst
@@ -11,4 +11,4 @@ let v_assume (v__formula: bool) = assume v__formula
 
 unfold let v_exists (v__f: 'a -> Type0): Type0 = exists (x: 'a). v__f x
 unfold let v_forall (v__f: 'a -> Type0): Type0 = forall (x: 'a). v__f x
-unfold let implies (lhs: bool) (rhs: bool): bool = (not lhs) || rhs
+unfold let implies (lhs: bool) (rhs: unit -> bool): bool = (not lhs) || rhs ()