fact: Fixpoint eval_hyps_bnd (hyps : list I.type) (vars : list R) := match hyps, vars with | hh :: th, hv :: tv => contains (I.convert hh) (Xreal hv) /\ eval_hyps_bnd th tv | nil, nil => True | _, _ => False end.
imports: Coq(Reals Psatz) Flocq(Raux) Coq(List) Xreal Interval Tree Prog