Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)

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).

Thanks for the MR and welcome!

This mostly looks good modulo some small nits.

added 1 commit

• 8f98c736 - Minor style tweaks

Compare with previous version

Okay, I think that should cover everything you mentioned?

resolved all threads

Looks great. Thanks! Merging.

mentioned in commit 99bad668

merged