fact: Fixpoint eval (vs : Vars V) (P : Pol) : R := match P with | Pconst c => phi c | PX P v Q => (eval vs P) * (vs v) + (eval vs Q) end.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings