fact: Fixpoint uncurrify {Tl} := match Tl return evalExprTypeRounded_fun Tl -> evalExprTypeRounded_list Tl -> Prop with | nil => fun f l => f | _ :: Tl' => fun f l => uncurrify (f (fst l)) (snd l) end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)