fact: Definition build_not2 i f := foldi (fun _ (f' : BFormula (Formula Z) isProp) => NOT (NOT f')) 0 i f.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz