fix error in SELECT_AX and then prove it consistent

this doesn't actually require is_choice, i.e. we don't have to
explicitly designate the choice function in the set theory, because we
specify the semantics of select indirectly via its axiom.