proposition: Lemma list_var_correct2 : forall Tl (l : evalExprTypeReal_list Tl) n, evalCArithExpr2 (nth n (list_var (length Tl)) (CInt 0)) (toList l) = nthExprTypeReal n l 0.
proof: Proof. induction Tl as [| T' Tl]; destruct n; [easy | easy | easy |]. simpl length. simpl toList. change (CInt 0) with (Psucc (CInt 0)). unfold list_var in *. rewrite nth_list_var_aux_S. rewrite evalCArithExpr2_succ. now rewrite 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