fix proof of env_rs_empty

broken by minor change to EVAL of LENGTH in HOL.
fix compile_top_thm

SUM_ACC