add Countable instance for decidable Sigma types

This instance became useful when working with, e.g., a type for elements of a set { a : A | a ∈ X } and wanting to construct a gmap with this domain.