diff --git a/theories/examples/abs_hashtable.v b/theories/examples/abs_hashtable.v
index 3ef61ba0465590951475449e7b7c371f93651b84..6fb5d1e5d64483037ccf2321b978a5893d35e0a4 100644
--- a/theories/examples/abs_hashtable.v
+++ b/theories/examples/abs_hashtable.v
@@ -162,8 +162,9 @@ Lemma index_of'_spec (k : Z) (m: list Z) :
 Proof.
   destruct (index_of' m k) as [i|] eqn:Eq.
   - apply bind_Some in Eq as [[??] [Eq1 Eq2]]. simpl in Eq2. simplify_eq.
-    destruct (list_find_Some _ _ _ _ Eq1) as [Eq2 Eq3].
-    have FA := list_find_slice _ _ _ _ Eq1. repeat split.
+    have FA := list_find_slice _ _ _ _ Eq1.
+    apply list_find_Some in Eq1 as [Eq2 Eq3].
+     repeat split.
     + by eapply lookup_lt_Some.
     + apply (nth_lookup_Some _ _ 0%Z) in Eq2. naive_solver.
     + eapply Forall_impl; last eauto. move => /= z0. naive_solver.
@@ -246,7 +247,7 @@ Qed.
 Section Hashtable.
 
 Context {hf : hash_fun}.
-Hint Resolve size_pos hash_range.
+Hint Resolve size_pos hash_range : core.
 
 Definition hlookup (m : list Z) (k : Z) :=
   (index_of' (rebase m (hash k)) k) ≫= (λ i, Some $ (i + hash k) `mod` size).