fact: Definition EvalQuantifier (qvar : Var) (r : Expression) (e : Expression) (v : Value) (st : State.t) : Prop := let fr' := st@fr[quants:= VarDict.update st@fr@quants qvar v] in let e' := EvalBoolExpression e st[fr:=fr'] in let r' := EvalBoolExpression r st[fr:=fr'] in r' -> e'.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)