diff --git a/theories/sets.v b/theories/sets.v
index 3a81880c4317688300824c15d77306be2ed32d20..8c8bfba030255e19575eeeaa0d48674d799b6eef 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -883,6 +883,10 @@ Section fin_to_set.
 
   Lemma elem_of_fin_to_set a : a ∈ fin_to_set A.
   Proof. apply elem_of_list_to_set, elem_of_enum. Qed.
+
+  Global Instance set_unfold_fin_to_set a :
+    SetUnfoldElemOf a (fin_to_set A) True.
+  Proof. constructor. split; auto using elem_of_fin_to_set. Qed.
 End fin_to_set.