TLAPM parser does not accept implicit <*>/<+> proof step IDs with names

[ahelwer]

Related to (and possibly the cause of) #165. Whereas that issue was about referring to proof steps in the same level, this is about writing proof steps in a given level. The TLAPM parser does not accept names being added to steps with an implicit level. These two inputs will both fail:

---- MODULE Test ----
THEOREM TRUE
<*>abc 1
<*>def QED
====

---- MODULE Test ----
THEOREM TRUE
<1>abc 1
  <+>def 2
  <2>ghi QED
<1>jkl QED
====

Ref #159

[ahelwer]

Further experimentation with SANY's semantic checker in tlaplus/tlaplus#1133 shows this is expected behavior, and implicit steps should not have names; SANY gives this error:

<*> and <+> cannot be used for a named step.

These tests should be removed from the syntax corpus.