proposition: Theorem app_merge_hyps_eval_bnd : forall prec vars hyps consts, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> A.contains_all (compute_inputs prec hyps consts) (vars ++ map (fun c => eval c nil) consts).
proof: Proof. intros prec vars hyps consts He. unfold compute_inputs. revert vars He. induction (R.merge_hyps prec hyps) as [|h t IH]. intros [|vars]. 2: easy. intros _. simpl. split. now rewrite 2!map_length. intros n. rewrite (nth_map (Evar 0)). destruct le_lt_dec as [H|H]. now rewrite I.nai_correct. rewrite (nth_map_lt (Evar 0)) by easy. apply T.eval_bnd_correct. intros [|v vars]. easy. simpl. intros [H1 H2]. apply A.contains_all_cons with (2 := H1). now apply IH. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify