proposition: Lemma well_formed_list_var_aux {Tl} : forall (lR : evalExprTypeReal_list Tl) l, well_formed lR (map add_compatibility (list_var_aux (length Tl) (length l))) (l ++ toList lR).
proof: Proof. induction Tl; [easy |]. intros [xR lR] l. simpl. repeat split. - apply nth_middle. - rewrite <-(app_nil_l (toList lR)), app_comm_cons, app_assoc. rewrite <-(last_length l xR). apply IHTl. 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