Election, then publication: a win plus a successful client value starts a stable publication

import Definitions.Def_OpenSearchCoordination
import Definitions.Def_OpenSearchSafety
import Definitions.Def_OpenSearchProgress
import Definitions.Def_OpenSearchPreVote
open OpenSearchCoordination OpenSearchSafety OpenSearchProgress OpenSearchPreVote

theorem OpenSearchLiveness.election_then_publication {V : Type} (P : Params) (hP : P.InitCompatible)
    (hes : P.strategy = ElectionStrategy.DEFAULT_INSTANCE)
    (W : Cluster V) (hW : Reachable P W)
    (c : NodeId) (t : Nat) (Q : List NodeId)
    (hQ : ∀ q ∈ Q, P.eligible q = true)
    (hwon : (W.node c).electionWon = true) (hct : (W.node c).currentTerm = t)
    (s : ClusterState V) (cs' : CoordinationState V) (p : PublishRequest V)
    (hcv : (W.node c).handleClientValue s = .ok (cs', p))
    (hcontract : (W.node c).clientValueContract s)
    (hfields : cs'.electionWon = (W.node c).electionWon ∧
      cs'.currentTerm = (W.node c).currentTerm ∧
      cs'.lastCommittedConfiguration = (W.node c).lastCommittedConfiguration ∧
      cs'.lastAcceptedConfiguration = (W.node c).lastAcceptedConfiguration ∧
      cs'.lastPublishedVersion = s.version ∧ cs'.publishVotes.nodes = [])
    (hpacc : p.acceptedState = s)
    (hst : s.term = t)
    (hquorum : (W.node c).lastCommittedConfiguration.hasQuorum Q = true ∧
      (W.node c).lastAcceptedConfiguration.hasQuorum Q = true ∧
      s.lastCommittedConfiguration.hasQuorum Q = true ∧
      s.lastAcceptedConfiguration.hasQuorum Q = true)
    (hterm : ∀ q ∈ Q, (W.node q).currentTerm ≤ t) :
    ∃ W', PublicationExec P c t Q
        ((W.set c cs').send (.publishRequest c p.acceptedState
          (W.node c).lastAcceptedTerm (W.node c).lastAcceptedVersion)) W' ∧
      Committed W' t p.acceptedState.version := by sorry