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