the reason that the step fails is that for the backends your hypothesis Phase1b(a) gets coalesced into an anonymous predicate. For example, here is the input that Zenon receives:
;; obligation #1
$hyp "a_in" (TLA.in a Acceptors)
$hyp "m_in" (TLA.in m a_msgshash_primea)
$hyp "a_m1a_in" (TLA.in a_m1a msgs)
$hyp "v'152" (a_h97e32460362eba8559dabb07ccf5e9a a)
$goal (\/ (TLA.bEx Proposers ((p) (\/ (\/ (\/ (\/ (Phase1a p)
(a_Phase2a1a p)) (a_Phase2a11a p)) (a_Phase2a12a p)) (a_Phase2a13a p))))
(TLA.bEx Acceptors ((a_1) (\/ (\/ (Phase1b a_1) (Phase2b a_1)) (PhasePr a_1)))))
The hypothesis named "v'152" corresponds to Phase1b(a), and you can see that the predicate has been renamed and doesn't correspond to the one that appears in the conclusion. I don't have a clear explanation yet for why that happens, and I believe it is an error. My hunch is that the PM gets confused by the primed hypotheses in the enclosing SUFFICES steps <4> or <5> and then plays overly cautious. However, I can offer two workarounds:
1. Move your step further up in the proof hierarchy. For example, insert it immediately after step <2>6, like so:
<3>0. Next BY <2>6 DEF Next
Then, replace <5>6 by <3>0 in the justification of step <5>7.
2. Change lemma SafeAtStable by replacing "Next" on the left-hand side of the implication by "[Next]_vars", then you can omit step <5>6 altogether.
We'll again investigate the coalescing algorithm to understand what went wrong here. Thanks for reporting this.
Regards,
Stephan