proposition: Lemma eval_add' vs : forall P Q, eval vs (add P Q) = eval vs P + eval vs Q.
proof: Proof. induction P as [c|P1 IH1 v P2 IH2];intros Q. - simpl. apply eval_addC. - simpl. rewrite eval_add_aux;auto. rewrite IH2. apply plus_assoc. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings