fact: Fixpoint convertibleFloat_list {Tl} : evalExprTypeFloat_list Tl -> Prop := match Tl with | nil => fun lC => True | T :: _ => fun lC => convertibleFloat (fst lC) /\ convertibleFloat_list (snd lC) end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)