diff --git a/theories/finite.v b/theories/finite.v
index d24e9c1ebc628bab92809236d2f943b06b6033c2..8d52436a2c993c27375f55f6f66c180983f07474 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -361,3 +361,39 @@ Next Obligation.
 Qed.
 Lemma fin_card n : card (fin n) = n.
 Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
+
+Section sig_finite.
+  Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
+
+  Fixpoint list_filter_sig (l : list A) : list (sig P) :=
+    match l with
+    | [] => []
+    | x :: l => match decide (P x) with
+              | left H => x ↾ H :: list_filter_sig l
+              | _ => list_filter_sig l
+              end
+    end.
+  Lemma list_filter_sig_filter (l : list A) :
+    proj1_sig <$> list_filter_sig l = filter P l.
+  Proof.
+    induction l as [| a l IH]; [done |].
+    simpl; rewrite filter_cons.
+    destruct (decide _); csimpl; by rewrite IH.
+  Qed.
+
+  Context `{Finite A} `{∀ x, ProofIrrel (P x)}.
+
+  Global Program Instance sig_finite : Finite (sig P) :=
+    {| enum := list_filter_sig (enum A) |}.
+  Next Obligation.
+    eapply NoDup_fmap_1. rewrite list_filter_sig_filter.
+    apply NoDup_filter, NoDup_enum.
+  Qed.
+  Next Obligation.
+    intros p. apply (elem_of_list_fmap_2_inj proj1_sig).
+    rewrite list_filter_sig_filter, elem_of_list_filter.
+    split; [by destruct p | apply elem_of_enum].
+  Qed.
+  Lemma sig_card : card (sig P) = length (filter P (enum A)).
+  Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
+End sig_finite.
diff --git a/theories/list.v b/theories/list.v
index 61013ab690078dc9bb1d9e67c900a611135764b0..c0f62879df4aedf8645ebfc599f86f2f4c2daad8 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3474,6 +3474,14 @@ Section fmap.
   Proof.
     naive_solver eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
   Qed.
+  Lemma elem_of_list_fmap_2_inj `{!Inj (=) (=) f} l x : f x ∈ f <$> l → x ∈ l.
+  Proof.
+    intros (y, (E, I))%elem_of_list_fmap_2. by rewrite (inj f) in I.
+  Qed.
+  Lemma elem_of_list_fmap_inj `{!Inj (=) (=) f} l x : f x ∈ f <$> l ↔ x ∈ l.
+  Proof.
+    naive_solver eauto using elem_of_list_fmap_1, elem_of_list_fmap_2_inj.
+  Qed.
 
   Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
   Proof.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 9b2bbc38984c01704d992bde7cc3abfa5a4ae387..96974f754a6ab6e58c430e61382c6c4a5f003d7d 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -38,6 +38,9 @@ Proof.
   destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
   f_equal. apply proof_irrel.
 Qed.
+Instance proj1_sig_inj `(P : A → Prop) `{∀ x, ProofIrrel (P x)} :
+  Inj (=) (=) (proj1_sig (P:=P)).
+Proof. intros ??. apply (sig_eq_pi P). Qed.
 Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x : sig P) p : `x ↾ p = x.
 Proof. apply (sig_eq_pi _); reflexivity. Qed.