diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index d15bfcfb8571c6d2cfe7d41759e509fa60edf33d..3c50fb3379361cbb366fa04e4aec383a9ca5f551 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -475,7 +475,7 @@ Proof.
   - intros [X Hfin]. exists (elements X). set_solver.
 Qed.
 
-Lemma dec_pred_finite_set (P : A → Prop) {Hdec : ∀ x : A, Decision (P x)} :
+Lemma dec_pred_finite_set (P : A → Prop) `{!∀ x : A, Decision (P x)} :
   pred_finite P ↔ (∃ X : C, ∀ x, P x ↔ x ∈ X).
 Proof.
   rewrite dec_pred_finite; [|done]. split.
diff --git a/theories/finite.v b/theories/finite.v
index 6436fae23ad629b495c071701344c0f4fbd34561..9aac9ff0077feab5b2f99978eabf749cf9d63939 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -381,24 +381,21 @@ Proof.
 Qed.
 
 (* shouldn’t be an instance (cycle with [sig_finite]): *)
-Lemma finite_sig_dec {A} {Heqdec : EqDecision A} (P : A → Prop) `{Hfin : Finite (sig P)} :
-  ∀ x, Decision (P x).
+Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
+  Decision (P x).
 Proof.
-  intros x. destruct Hfin as [elems _ Helems'].
-  assert (∀ px, (x ↾ px) ∈ elems) as Helems by done; clear Helems'.
-  assert (Decision {px | (x ↾ px) ∈ elems}) as [[px ?] | no_px].
-  {
-    induction elems as [ | [y py] elems' IH].
-    { right. intros [? ?%not_elem_of_nil]. naive_solver. }
-    { destruct (decide (x = y)) as [-> | ?].
-      { left. by exists py. }
-      { destruct IH as [[px ?] | no_px].
-        { intros px. specialize (Helems px) as ?%elem_of_cons. naive_solver. }
-        { left. by exists px. }
-        { right. intros [px ?%elem_of_cons]. naive_solver. } } }
-  }
-  { by left. }
-  { right. intros px. apply no_px. by exists px. }
+  assert (∀ px, (x ↾ px) ∈ enum (sig P)) as Helems by auto using elem_of_enum.
+  assert (Decision {px | (x ↾ px) ∈ enum (sig P)}) as [[px ?]|Hno_px].
+  { induction (enum _) as [ | [y py] elems IH].
+    { right. by intros [? ?%not_elem_of_nil]. }
+    destruct (decide (x = y)) as [-> | ?].
+    { left. exists py. by left. }
+    destruct IH as [[px ?]|?].
+    { intros px. specialize (Helems px) as ?%elem_of_cons. naive_solver. }
+    - left. by exists px.
+    - right. intros [px ?%elem_of_cons]. naive_solver. }
+  - by left.
+  - right. intros px. apply Hno_px. by exists px.
 Qed.
 
 Section sig_finite.
diff --git a/theories/sets.v b/theories/sets.v
index 27925908936cedc30c3b28a1f565997bbafef58f..09049410e38688f738c8a9cbbaf68eb0fbdd0353 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1188,24 +1188,24 @@ Proof.
   { exists ys. revert IH1. rewrite !drop_ge, app_nil_r; [done|lia..]. }
 Qed.
 
-Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Hfin : Finite (sig P)} :
+Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} :
   pred_finite P.
 Proof.
   exists (proj1_sig <$> enum _). intros x px.
   apply elem_of_list_fmap_1_alt with (x ↾ px); [apply elem_of_enum|]; done.
 Qed.
 
-Lemma pred_finite_arg2 {A B} (P : A → B → Prop) :
-  pred_finite (uncurry P) → ∀ x, pred_finite (P x).
+Lemma pred_finite_arg2 {A B} (P : A → B → Prop) x :
+  pred_finite (uncurry P) → pred_finite (P x).
 Proof.
-  intros [xys ?] x. exists (xys.*2). intros y ?.
+  intros [xys ?]. exists (xys.*2). intros y ?.
   apply elem_of_list_fmap_1_alt with (x, y); by auto.
 Qed.
 
-Lemma pred_finite_arg1 {A B} (P : A → B → Prop) :
-  pred_finite (uncurry P) → ∀ y, pred_finite (flip P y).
+Lemma pred_finite_arg1 {A B} (P : A → B → Prop) y :
+  pred_finite (uncurry P) → pred_finite (flip P y).
 Proof.
-  intros [xys ?] y. exists (xys.*1). intros x ?.
+  intros [xys ?]. exists (xys.*1). intros x ?.
   apply elem_of_list_fmap_1_alt with (x, y); by auto.
 Qed.