Cardinality results for sets of lists drawing from some underlying set

Allows a simplification of the earlier result stating that infinite
sets are in bijection with their finite subsets.

Introduces "list" as a new constant name.