fact: Definition build_pexpr := foldi (fun i cont vm h => build_pexpr_atom_aux cont vm (get_atom h)) 0 (PArray.length t_atom) (fun vm _ => (vm,PEc 0%Z)).
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz