fact: Definition build_op2 op := match op with | (BO_eq Typ.TZ) => Some OpEq | BO_Zle => Some OpLe | BO_Zge => Some OpGe | BO_Zlt => Some OpLt | BO_Zgt => Some OpGt | _ => None end.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz