fact: Definition QuantIdentityElement (q : Quantifier) : Int.t := match q with | Sum => Int.const 0 | Product => Int.const 1 | Min => Int.const MaxInt | Max => Int.const MinInt | _ => Int.const 0 end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)