fact: Definition bounded_formula (p:positive) (f:Formula Z) := bounded_pexpr p (f.(Flhs)) && bounded_pexpr p (f.(Frhs)).
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz