util work - almost finished finite_set_list_length

Almost finished proving all of the supporting lemmas and theorems to
prove that a NoDup list built from members of a finite set has finite
length (that is, any such list must have length <= the cardinality of
the set).

Finishing this should lead quickly to the minimal member proof.