fact: Definition check_micromega cl c : C.t := match build_clause empty_vmap cl with | Some (_, bf) => if ZTautoChecker bf c then cl else C._true | None => C._true end.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz