proposition: Lemma eval_toPol@{} vs : forall e : Expr V, eval vs (toPol e) = Quoting.eval _ vs e.
proof: Proof. induction e as [v| | |a IHa b IHb|a IHa b IHb|a IHa];simpl. - rewrite (preserves_1 (f:=phi)),(preserves_0 (f:=phi)),plus_0_r,mult_1_l. reflexivity. - apply preserves_0. - apply preserves_1. - rewrite eval_add,IHa,IHb. reflexivity. - rewrite eval_mul,IHa,IHb. reflexivity. - rewrite eval_mulC. rewrite (almostring_mor_neg (f:=phi)),preserves_1. rewrite <-almost_ring_neg_pr. apply ap,IHa. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings