vs : forall c P, eval vs (addC c P) = (phi c) + eval vs P. Proof. induction P;simpl. - apply preserves_plus. - rewrite IHP2. rewrite 2!plus_assoc. rewrite (plus_comm (phi c)). reflexivity. Qed.
Require Import Import Quoting.