fact: Definition build_var := foldi (fun i cont vm h => build_hform cont vm (get_form h)) 0 (PArray.length t_form) (fun _ _ => None).
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz