Hi,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 NextThen, 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,StephanOn 12 Feb 2018, at 19:36, saksha...@xxxxxxxxxxxxxx wrote:Hi,Line 3403 of the attached tla file has the following obligation which fails on TLAPS(Version 1.5.6 of 29 January 2018) on my machine (Ubuntu 17.10):  <5>6. Next BY <2>6 DEF Nextwhere  Next == \/ \E p \in Proposers : Phase1a(p) \/ Phase2a1(p) \/ Phase2a11(p) \/ Phase2a12(p) \/ Phase2a13(p)          \/ \E a \in Acceptors : Phase1b(a) \/ Phase2b(a)  \/ PhasePr(a)and <2>6 is  <2>6. ASSUME NEW a \in Acceptors,               Phase1b(a)        PROVE  Inv'Also attached is the screenshot showing the interesting obligations. I'm wondering if I'm making a really dumb mistake here or is it something else?Thanks,Saksham Chand -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx. To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.