proposition: Lemma eval_mulC vs : forall c P, eval vs (mulC c P) = (phi c) * eval vs P.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings