proposition: Fact eval_poly sigma p : eval (sigma >> iμ) (embed_poly p) = iμ (dp_eval_pfree sigma p).
proof: Proof. Proof using ext_model FA_model. induction p; cbn. - now rewrite eval_num. - reflexivity. - destruct d; cbn. + now rewrite IHp1, IHp2, add_hom. + now rewrite IHp1, IHp2, mult_hom. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullFacts Semantics.Tarski.FullSoundness) Undecidability.FOL.PA Undecidability.FOL.Arithmetics(TarskiFacts DeductionFacts NatModel) Undecidability.H10(H10p) List Lia