I've added an instance sig_finite along with a couple of minor things used to define/prove it. This is a Finite instance for sigs over Finite types whose predicates are decidable and proof irrelevant:
(* Not a direct excerpt. *)
Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} `{∀ x, ProofIrrel (P x)}.
Global Instance sig_finite : Finite (sig P).