vs : forall c P, eval vs (mulC c P) = (phi c) * eval vs P. Proof. induction P as [d | P1 IH1 v P2 IH2];simpl. - apply preserves_mult. - rewrite eval_PXguard. rewrite IH1,IH2,plus_mult_distr_l,mult_assoc. reflexivity. Qed.
Require Import Import Quoting.