diff --git a/theories/finite.v b/theories/finite.v
index 6bd7d4af78781c5af2c000952d00e492c0864b32..767a31c139173eaf58cc3933e43782dcc9ab6a6a 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -64,7 +64,8 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
 Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
   intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
-  rewrite Hi; simpl. rewrite !Nat2Pos.id by done. simpl.
+  rewrite Hi. unfold decode_nat, decode. simpl. rewrite !Nat2Pos.id by done.
+  simpl.
   apply list_find_Some in Hi; naive_solver.
 Qed.