proposition: Lemma evalCArithExpr2_succ : forall t l x, evalCArithExpr2 (Psucc t) (x :: l) = evalCArithExpr2 t l.
proof: Proof. induction t as [| | | OP | | | | |]; simpl; intros. 5, 6, 7, 9: now rewrite IHt. 1, 2, 3: easy. - now destruct OP; rewrite IHt1, IHt2. - now rewrite IHt1; rewrite IHt2. 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