fact: Definition EvalRequires (sc : SpecificationCase) (st : State.t) : Prop := forall r , r = CASE.requires sc -> match REQUIRES.pred r with | (:expr:) => EvalPredicate expr st | \not_specified => NotSpecifiedRequires end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)