Correctness of refinement mapping

Hi. This question is similar to one that has been asked before (but perhaps with a different focus):

As far as I understand, every TLA+ spec-mapping (INSTANCE/WITH) that is "simple", i.e. does not require auxiliary variables, is indeed a refinement mapping. But once auxiliary variables are needed, things are not so clear. Abadi and Lamport proved that if specification B implements A, then, provided B satisfies some reasonable conditions, there is a refinement mapping from any B behavior to an A behavior, that possibly requires auxiliary history and/or prophecy variables. What isn't clear to me is the opposite direction: given a mapping from B to A that has auxiliary variables, how do we ensure that it is a valid refinement mapping, namely that every added variable indeed satisfies the requirements of a history/prophecy variable?

I am working on a reduction in the same vein as the ones discussed in this paper (by Cohen and Lamport), and while I believe I can get a "working" mapping with auxiliary variables, I get the sense that checking that the auxiliary variables are valid histories/prophecies is no easier than checking my original hypothesis (that B implements A). Short of model checking for hidden variables, is there a way TLC can assist in ensuring the validity of a refinement mapping?

Ron