Close missing BY clauses in TypeOK_Step network cases

Two `<7>. QED` steps in the `n2 # to` and `n2 # self` branches of
`<5>1` lacked any justification, leaving the lemma incomplete. A bare
`<n>. QED` without `BY`/`OBVIOUS` is silently accepted by tlapm and
generates zero obligations (cf. tlaplus/tlapm#271), so the gap was not
caught at the time the proof was originally added in #211.

Reported post-merge by @tangruize in
#211 (comment),
who flagged this exact anti-pattern while investigating the bare-QED
behavior. Fix: name the preceding `network'[n2] = network[n2]` step
as `<7>1` (since unnamed steps cannot be cited) and have QED close
via `BY <7>1`, mirroring the parallel `<6>1` cases. All 316
obligations in the surrounding range verify cleanly.

Refs: #211

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Co-authored-by: Ruize Tang <tangruize@users.noreply.github.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: 3 people

specifications/ewd998/EWD998PCal_proof.tla

@@ -621,9 +621,9 @@ LEMMA TypeOK_Step ==
                 BY <7>2, <4>2, BagAddPreservesToks
               <7>. QED  BY <6>1, <7>3
             <6>2. CASE n2 # to
-              <7>. network'[n2] = network[n2]
+              <7>1. network'[n2] = network[n2]
                 BY <4>1, <6>2
-              <7>. QED
+              <7>. QED  BY <7>1
             <6>. QED  BY <6>1, <6>2
           <5>. QED  BY <5>1, <4>0a
         <4>5. \E n \in Node : \E t \in DOMAIN network'[n] :
@@ -709,9 +709,9 @@ LEMMA TypeOK_Step ==
                 BY <7>2, <4>2, BagRemovePreservesToks
               <7>. QED  BY <6>1, <7>3
             <6>2. CASE n2 # self
-              <7>. network'[n2] = network[n2]
+              <7>1. network'[n2] = network[n2]
                 BY <4>1, <6>2
-              <7>. QED
+              <7>. QED  BY <7>1
             <6>. QED  BY <6>1, <6>2
           <5>. QED  BY <5>1, <4>0a
         <4>5. \E n \in Node : \E t \in DOMAIN network'[n] :