fact: Definition EvalBinaryBoolOp (op : BinaryBoolOp) (b1 : Prop) (b2 : Prop) : Prop := match op with | BoolEquality => b1 <-> b2 | BoolInequality | LogicalXor => not (b1 <-> b2) | LogicalAnd => b1 /\ b2 | LogicalOr => b1 \/ b2 end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)