proposition: Lemma max_arity_correct : forall e vars v, max_arity e (length vars) = true -> eval e (vars ++ v) = eval e vars.
proof: Proof. induction e as [n|o|o e IH|o e1 IH1 e2 IH2] ; simpl ; intros vars v H. - apply app_nth1. now apply Nat.ltb_lt. - easy. - now rewrite IH. - rewrite <- Bool.andb_lazy_alt in H. apply andb_prop in H. rewrite IH1 by easy. now rewrite IH2. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree