theorem AP.AStrat.histBlind_def {a : AStrat} : a.HistBlind ↔ a.WF ∧ ∀ (s : State) (hist : List PointZ), AState s → sys.WF (s.setHist hist) → sys.hasTr s → a.f (s.setHist hist) = a.f s

theorem AP.DStrat.histBlind_def {d : DStrat} : d.HistBlind ↔ d.WF ∧ ∀ (s : State) (hist : List PointZ), DState s → sys.WF (s.setHist hist) → sys.hasTr s → d.f (s.setHist hist) = d.f s

instance AP.instWFOfHistBlind {a : AStrat} [ha : a.HistBlind] : a.WF

instance AP.instWFOfHistBlind_1 {d : DStrat} [hd : d.HistBlind] : d.WF

instance AP.instHistBlindDefaultAStrat : default.HistBlind

instance AP.instHistBlindDefaultDStrat : default.HistBlind