proposition: Fact standard_embed_poly rho p f : extensional I -> (forall d, iμ (f d) = d) -> eval rho (embed_poly p) = iμ (dp_eval_pfree (rho >> f) p).
proof: Proof. Proof using FA_model. intros HI Hf. induction p; try destruct d; cbn. - apply eval_num. - unfold funcomp. now rewrite Hf. - rewrite IHp1, IHp2. rewrite add_hom; trivial. firstorder. - rewrite IHp1, IHp2. rewrite mult_hom; trivial. firstorder. 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