How can this lemma (involving []) be applied?

[Roy Overbeek <r.over...@xxxxxxxxx>]

Hi,

I am studying TLA+ and have written a specification Spec of a toy bank account. TypeOK asserts (among others) that balance \in Nat. I have already proven:

  THEOREM TypeOKInvariant == Spec => []TypeOK

I would now like to prove the corollary

  COROLLARY BGZInvariant == Spec => []BalanceGeqZero

where

  BalanceGeqZero == balance >= 0.

To this end, I have first successfully proven a general lemma:

LEMMA BoxImpl == ASSUME NEW P,
                        NEW Q,
                        P => Q,
                        []P
                 PROVE  []Q

My current proof for BGZInvariant is then:    
  
COROLLARY BGZInvariant == Spec => []BalanceGeqZero
  <1> SUFFICES ASSUME Spec              \* Proof succeeds.
               PROVE []BalanceGeqZero
    OBVIOUS
  <1>1 TypeOK => BalanceGeqZero         \* Proof succeeds.
    BY DEFS TypeOK, BalanceGeqZero
  <1>2 []TypeOK                         \* Proof succeeds.
    BY TypeOKInvariant 
  <1> QED                               \* Proof fails. Why?
    BY BoxImpl, <1>1, <1>2

I do not understand why the QED step fails. I have tried a similar setup with a lemma not involving [], and that worked, so it seems to be that P and Q should be instantiatable with respectively TypeOK and BalanceGeqZero. Adding PTL does not help, and I have so far not been able to find a solution in the literature.

Any help would be much appreciated.

Roy