Begin cleaning up defn. of reach-closed semantics
Add vals_def condition to Clight at_external/halted
Further progress on RC cleanup
Push new rclosed through ret_lemmas
Push through new RC condition