diff --git a/hackernews3.mlw b/hackernews3.mlw
index cd5dad0..eb53426 100644
--- a/hackernews3.mlw
+++ b/hackernews3.mlw
@@ -7,7 +7,7 @@ module GenericBinarySearch
   let binary_search (pred: int -> bool) (low: int) (high: int): int
     requires { pred low = False }
     requires { pred high = True }
-    requires { forall i j. i <= j -> (pred i -> pred j) }
+    requires { low < high }
     ensures  { pred result = False /\ pred (result + 1) = True }
   =
     let cur_low = ref low in
@@ -15,6 +15,7 @@ module GenericBinarySearch
 
     while !cur_high - !cur_low > 1 do
       variant { !cur_high - !cur_low }
+      invariant { !cur_low < !cur_high }
       invariant { pred !cur_low = False /\ pred !cur_high = True }
 
       let mid = div (!cur_high + !cur_low) 2 in