eval_addX'@{} vs : forall c (v:V) Q, eval vs (addX' c v Q) = phi c * vs v + eval vs Q. Proof. induction Q as [d|Q1 IH1 w Q2 IH2]. - simpl. reflexivity. - simpl. pose proof (tricho_compare_eq v w) as E. destruct (v ?= w);[clear E|rewrite <-E by split;clear E w|clear E]. + simpl. rewrite IH2. rewrite 2!plus_assoc. apply ap011;trivial. apply plus_comm. + simpl. rewrite eval_addC. rewrite plus_mult_distr_r. symmetry;apply plus_assoc. + simpl. reflexivity. Qed.
Require Import Import Quoting.