theorem AP.State.aHws_iff_aHws_histBlind_both {s : State} [hs : sys.WF s] : s.aHws ↔ ∃ (a : AStrat), a.HistBlind ∧ ∀ (d : DStrat), d.HistBlind → s.aWins { a := a, d := d }

theorem AP.State.dHws_iff_dHws_histBlind_both {s : State} [hs : sys.WF s] : s.dHws ↔ ∃ (d : DStrat), d.HistBlind ∧ ∀ (a : AStrat), a.HistBlind → s.dWins { a := a, d := d }