fact: Definition EvalBoolConditional (c : Expression) (t : Expression) (e : Expression) (st : State.t) : Prop := let bc := EvalBoolExpression c st in let bt := EvalBoolExpression t st in let be := EvalBoolExpression e st in (bc -> bt) /\ (~bc -> be).
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)