proposition: Theorem eval_hyps_bnd_correct : forall prec hyps vars (g : Prop), (eval_hyps_bnd (merge_hyps prec hyps) vars -> g) -> eval_hyps hyps vars g.
proof: Proof. intros prec. induction hyps as [|h1 t1 IH1]. intros [|x vars] g H. now apply H. exact I. intros [|x vars]. easy. simpl. generalize I.whole (I.whole_correct x). induction h1 as [|h2 t2 IH2] ; intros xi Ix g H. apply IH1. intros H'. now apply H. simpl. intros H'. simpl in H. apply (IH2 (I.meet (eval_hyp_bnd prec h2) xi)). apply I.meet_correct with (2 := Ix). now apply eval_hyp_bnd_correct. intros H''. now apply H. Qed.
imports: Coq(Reals Psatz) Flocq(Raux) Coq(List) Xreal Interval Tree Prog