Reuse Inv in three Spec => [](TypeOK /\ Safety) theorem statements

Three of the proof files defined an inductive invariant Inv equal to
the body of the box of the theorem they were about to prove, then
restated that body verbatim on the right-hand side of the theorem.
Replace each "Spec => [](X /\ Y)" with "Spec => []Inv" so the
relationship "this theorem is exactly Inv being inductive" is
syntactically obvious and there is one place to keep in sync.

Affected files:

  transaction_commit/TCommit_proof.tla
    - THEOREM TCorrect == TCSpec => [](TCTypeOK /\ TCConsistent)
    + THEOREM TCorrect == TCSpec => []Inv

  byihive/VoucherLifeCycle_proof.tla
    - THEOREM Spec_TypeOK_Consistent == VSpec => [](VTypeOK /\ VConsistent)
    + THEOREM Spec_TypeOK_Consistent == VSpec => []Inv

  KeyValueStore/KeyValueStore_proof.tla
    - THEOREM TypeAndLifecycle == Spec => [](TypeInvariant /\ TxLifecycle)
    + THEOREM TypeAndLifecycle == Spec => []Inv

The original theorem statement (with the conjunction expanded) is
preserved in the doc comment at the top of each proof file so the
mapping back to the spec's theorem remains discoverable.

Other proof files in the branch use Inv without restating its body
on the antecedent already (e.g. SpecifyingSystems/.../InternalMemory_proof.tla
proves "LEMMA InvInductive == ISpec => []Inv" and exposes the
spec-shaped corollary via a separate "THEOREM TypeCorrect ==
ISpec => []TypeInvariant  BY InvInductive, PTL DEF Inv").  This
commit brings the three remaining files in line with that idiom.

All three proofs re-checked with TLAPS:
  - TCommit_proof.tla:           16  obligations
  - VoucherLifeCycle_proof.tla:  6   obligations
  - KeyValueStore_proof.tla:     28  obligations

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

Author: lemmy

specifications/KeyValueStore/KeyValueStore_proof.tla

@@ -8,7 +8,7 @@ EXTENDS KeyValueStore, TLAPS
 
 Inv == TypeInvariant /\ TxLifecycle
 
-THEOREM TypeAndLifecycle == Spec => [](TypeInvariant /\ TxLifecycle)
+THEOREM TypeAndLifecycle == Spec => []Inv
 <1>1. Init => Inv
   BY DEF Init, Inv, TypeInvariant, TxLifecycle, Store
 <1>2. Inv /\ [Next]_<<store, tx, snapshotStore, written, missed>> => Inv'

specifications/byihive/VoucherLifeCycle_proof.tla

@@ -9,7 +9,7 @@ EXTENDS VoucherLifeCycle, TLAPS
 
 Inv == VTypeOK /\ VConsistent
 
-THEOREM Spec_TypeOK_Consistent == VSpec => [](VTypeOK /\ VConsistent)
+THEOREM Spec_TypeOK_Consistent == VSpec => []Inv
 <1>1. VInit => Inv
   BY DEF VInit, Inv, VTypeOK, VConsistent
 <1>2. Inv /\ [VNext]_<<vState, vlcState>> => Inv'

specifications/transaction_commit/TCommit_proof.tla

@@ -8,7 +8,7 @@ EXTENDS TCommit, TLAPS
 
 Inv == TCTypeOK /\ TCConsistent
 
-THEOREM TCorrect == TCSpec => [](TCTypeOK /\ TCConsistent)
+THEOREM TCorrect == TCSpec => []Inv
 <1>1. TCInit => Inv
   BY DEF TCInit, Inv, TCTypeOK, TCConsistent
 <1>2. Inv /\ [TCNext]_rmState => Inv'