fact: Definition build_clause vm cl := match build_clause_aux vm cl with | Some (vm, bf) => Some (vm, IMPL bf None (FF isProp)) | None => None end.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz