class AP.AStrat.HistBlind (a : AStrat) : Prop

• wf : a.WF
• h (s : State) (hist : List PointZ) : AState s → sys.WF (s.setHist hist) → sys.hasTr s → a.f (s.setHist hist) = a.f s

class AP.DStrat.HistBlind (d : DStrat) : Prop

• wf : d.WF
• h (s : State) (hist : List PointZ) : DState s → sys.WF (s.setHist hist) → sys.hasTr s → d.f (s.setHist hist) = d.f s