prove in_fun_equals

had to duplicate range_in_fun_conv; can't put it in reflectionLib since
it depends on definitions in reflectionTheory