Revert "Weaken RC init to take reach-closure in m"

Reason: It's not necessary to take the reach-closure initially.
The effect bound on coresteps is already reach-closed.
Also: taking reach-closure initially is inconsistent with
the current treatment of return values in the RC aft_ext axiom.

This reverts commit c03334aafd2f26e8d393ddd9cd52be196bc22f9c.