proposition: Lemma rev_formula : forall A formula terms (ops : operations A), eval_generic ops formula terms = fold_right (fun y x => eval_generic_body ops x y) terms (rev formula).
proof: Proof. intros. pattern formula at 1 ; rewrite <- rev_involutive. unfold eval_generic, eval_generic_body. rewrite <- fold_left_rev_right. rewrite rev_involutive. apply refl_equal. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree