proposition: Corollary well_formed_list_var {Tl} : forall (lR : evalExprTypeReal_list Tl), well_formed lR (map add_compatibility (list_var (length Tl))) (toList lR).
proof: Proof. intros lR. rewrite <-(app_nil_l (toList lR)). unfold list_var. fold (@length R nil). apply well_formed_list_var_aux. Qed.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr