proposition: Lemma eval_exprsucc : forall t l x, Tree.eval (exprsucc t) (x :: l) = Tree.eval t l.
proof: Proof. now induction t; simpl; intros; [| | rewrite IHt | rewrite IHt1, 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