more thoughts about range_to_in

define good_range_to_in (this I'm least sure about), then define a
select_fun that takes range_to_in as a parameter. prove that it is
good_select, and prove the connection between inner and outer select
(select_thm) under the assumptions:
  good_range_to_in range_to_in and
  range_to_in (range ina) = ina
(for the particular ina at hand)

I guess this still might not work because range_to_in's type variable
can only be instantiated in one way.