removed some unnecessary steps from runiq_alt proof