fact: Definition refine_root prec depth hyps px cx pf cf pg cg g := let hyps := R.merge_hyps prec hyps in let xi := nth 0 (A.BndValuator.eval prec px (hyps ++ map (T.eval_bnd prec) cx)) I.nai in let check := check_goal prec hyps pg cg g in refine_root_aux depth prec pf (hyps ++ map (T.eval_bnd prec) cf) xi check.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify Interval_helper