mostly cosmetic changes to env_rs

but also add that rs.next_global is equal to LENGTH bs.globals. I think
this should hold...
prove env_rs_change_clock