proposition: Lemma eval_addC vs : forall c P, eval vs (addC c P) = (phi c) + eval vs P.
proof: Proof. induction P;simpl. - apply preserves_plus. - rewrite IHP2. rewrite 2!plus_assoc. rewrite (plus_comm (phi c)). reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings