prove is_set_theory holds for a specific example

based on the universe of :'a list.

existence proved by using the natural encoding of finite sets, via the
binary numerals for the lengths of the lists (and taking all the list
elements to be equal).

but the type variable means it won't be inconsistent to assume that
there is actually an infinite set, as will be necesary to further show
that is_model holds.
prove is_model for the list model, assuming an infinite set exists