fact: Fixpoint merge l p := match l with | nil => p | i :: l' => merge l' (CAnd p (CAtom i)) end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr