TLAPM parser does not accept proof step references in QED BY with implicit <*> proof level

[ahelwer]

This syntax fragment will fail parsing:

---- MODULE Test ----
THEOREM TRUE
PROOF
  <1>a TRUE
  <1>b QED BY <*>a
====

Ref #159

[ahelwer]

While #170 was indeed a false bug (you can't define implicit proof steps with names), this one is certainly real - SANY supports using <*>name to refer to numbered & named steps of the same level.