finish compile_prog_thm

by adding an extra assumption about the map generated by prog_to_i1 only
containing "it" if the semantic environment does. This can probably be
discharged by proving some separate theorem about prog_to_i1.